let x, y, p, q be real number ; :: thesis: for n being Element of 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 < ((abs x) * p) + ((abs y) * q)
let n be Element of 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 < ((abs x) * p) + ((abs 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 < ((abs x) * p) + ((abs 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 < ((abs x) * p) + ((abs y) * q) )
assume that
A1: ( e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 ) and
A2: e5 = (x * p1) + (y * p3) and
A3: e6 = (x * p2) + (y * p4) and
A4: dist e1,e2 < p and
A5: dist e3,e4 < q and
A6: x <> 0 and
A7: y <> 0 ; :: thesis: dist e5,e6 < ((abs x) * p) + ((abs y) * q)
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4 as Element of REAL n by A1, EUCLID:25;
A8: REAL n = n -tuples_on REAL by EUCLID:def 1;
A9: dist e5,e6 = |.(((x * f1) + (y * f3)) - ((x * f2) + (y * f4))).| by A1, A2, A3, SPPOL_1:20
.= |.(((x * f1) - (x * f2)) + ((y * f3) - (y * f4))).| by A8, Th9
.= |.((x * (f1 - f2)) + ((y * f3) - (y * f4))).| by A8, Th7
.= |.((x * (f1 - f2)) + (y * (f3 - f4))).| by A8, Th7 ;
A10: ( dist e1,e2 = |.(f1 - f2).| & dist e3,e4 = |.(f3 - f4).| ) by SPPOL_1:20;
|.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + |.(y * (f3 - f4)).| by EUCLID:15;
then |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= |.(x * (f1 - f2)).| + ((abs y) * |.(f3 - f4).|) by EUCLID:14;
then A11: |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) by EUCLID:14;
( 0 < abs x & 0 < abs y ) by A6, A7, COMPLEX1:133;
then ( (abs x) * |.(f1 - f2).| < (abs x) * p & (abs y) * |.(f3 - f4).| < (abs y) * q ) by A4, A5, A10, XREAL_1:70;
then ((abs x) * |.(f1 - f2).|) + ((abs y) * |.(f3 - f4).|) < ((abs x) * p) + ((abs y) * q) by XREAL_1:10;
hence dist e5,e6 < ((abs x) * p) + ((abs y) * q) by A9, A11, XXREAL_0:2; :: thesis: verum