let p, q, x, y be Real; :: thesis: for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < (|.x.| * p) + (|.y.| * q)
let n be Nat; :: thesis: for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < (|.x.| * p) + (|.y.| * q)
let e1, e2, e3, e4, e5, e6 be Point of (Euclid n); :: thesis: for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < (|.x.| * p) + (|.y.| * q)
let p1, p2, p3, p4 be Point of (TOP-REAL n); :: thesis: ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 implies dist (e5,e6) < (|.x.| * p) + (|.y.| * q) )
assume that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e3 = p3 and
A4: e4 = p4 and
A5: e5 = (x * p1) + (y * p3) and
A6: e6 = (x * p2) + (y * p4) and
A7: dist (e1,e2) < p and
A8: dist (e3,e4) < q and
A9: x <> 0 and
A10: y <> 0 ; :: thesis: dist (e5,e6) < (|.x.| * p) + (|.y.| * q)
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of REAL n by A1, A2, A3, A4, A5, A6, EUCLID:22;
A11: ( x * f2 = x * p2 & y * f4 = y * p4 ) by A2, A4;
( x * f1 = x * p1 & y * f3 = y * p3 ) by A1, A3;
then A12: f5 = (x * f1) + (y * f3) by A5;
A13: 0 < |.y.| by A10, COMPLEX1:47;
dist (e3,e4) = |.(f3 - f4).| by SPPOL_1:5;
then A14: |.y.| * |.(f3 - f4).| < |.y.| * q by A8, A13, XREAL_1:68;
A15: 0 < |.x.| by A9, COMPLEX1:47;
dist (e1,e2) = |.(f1 - f2).| by SPPOL_1:5;
then |.x.| * |.(f1 - f2).| < |.x.| * p by A7, A15, XREAL_1:68;
then A16: (|.x.| * |.(f1 - f2).|) + (|.y.| * |.(f3 - f4).|) < (|.x.| * p) + (|.y.| * q) by A14, XREAL_1:8;
|.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + |.(y * (f3 - f4)).| by EUCLID:12;
then |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + (|.y.| * |.(f3 - f4).|) by EUCLID:11;
then A17: |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= (|.x.| * |.(f1 - f2).|) + (|.y.| * |.(f3 - f4).|) by EUCLID:11;
dist (e5,e6) = |.(f5 - f6).| by SPPOL_1:5
.= |.(((x * f1) + (y * f3)) - ((x * f2) + (y * f4))).| by A6, A12, A11
.= |.(((x * f1) - (x * f2)) + ((y * f3) - (y * f4))).| by Th9
.= |.((x * (f1 - f2)) + ((y * f3) - (y * f4))).| by Th7
.= |.((x * (f1 - f2)) + (y * (f3 - f4))).| by Th7 ;
hence dist (e5,e6) < (|.x.| * p) + (|.y.| * q) by A17, A16, XXREAL_0:2; :: thesis: verum