Since you are going for a vector-based approach, I'd recommend to simplify that. Observe that all the concepts you are dealing with are invariant under affine transformations. I mean concepts such as “midpoint” and “collinear” as well as the ratio of distances along a line. So with that observation in mind, you are now free to apply an affine transformation to simplify coordinates without loss of generality. I'd recommend you make three of your for corners as (0,0),(1,0),(0,1). Then the whole configuration is driven by only two real numbers, namely the two coordinates of the fourth corner. Say (t,u) for example. That makes it very easy to compute concrete coordinates for everything, and thus show the expected colinearity. I doubt the distance inequalities actually play a role in that proof. I would expect that you get the conclusion without needing those inequalities at any point. Personally I'd do this computation with machinery from projective geometry, where the operations of connecting points and of intersecting lines can both be expressed as simple cross products of homogeneous coordinates so you'd avoid divisions. But that's mostly due to my background, and a non-projective formulation shouldn't be much different.
If you are not familiar with homogeneous coordinates, just read as the Cartesian coordinate vector . Since joining points and intersecting lines can both be computed using cross products, I got operations such as . I write not because for homogeneous coordinates, scalar multiples of the same vector represent the same point. So I've made it a habit to cancel common factors and to choose signs in such a way as to make the result aesthetically pleasing. The other relevant operation is midpoint, which in homogeneous coordinates I computed e.g. as
This corresponds to the you might do in Cartesian coordinates. The final determinant being zero demonstrates the requested collinearity: there is a line incident with all three points. If I were to express that line for Cartesian coordinates, it would be