let n be non zero Nat; :: thesis: for x, y, z being Element of REAL n holds (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))
let x, y, z be Element of REAL n; :: thesis: (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y))
( (Infty_dist n) . (x,y) in REAL & (Infty_dist n) . (x,z) in REAL & (Infty_dist n) . (z,y) in REAL ) ;
then reconsider sxy = sup (rng (abs (x - y))), sxz = sup (rng (abs (x - z))), szy = sup (rng (abs (z - y))) as Real by Def7;
sxy <= sxz + szy
proof
for er being ExtReal st er in rng (abs (x - y)) holds
er <= sxz + szy
proof
let er be ExtReal; :: thesis: ( er in rng (abs (x - y)) implies er <= sxz + szy )
assume er in rng (abs (x - y)) ; :: thesis: er <= sxz + szy
then consider i being object such that
A1: i in dom (abs (x - y)) and
A2: er = (abs (x - y)) . i by FUNCT_1:def 3;
(abs (x - y)) . i <= sxz + szy
proof
A3: (abs (x - y)) . i <= ((abs (x - z)) . i) + ((abs (z - y)) . i)
proof
reconsider fxy = x - y, fxz = x - z, fzy = z - y as complex-valued Function ;
A4: ( (abs fxy) . i = |.((x - y) . i).| & (abs fxz) . i = |.((x - z) . i).| & (abs fzy) . i = |.((z - y) . i).| ) by VALUED_1:18;
|.((x - y) . i).| <= |.((x - z) . i).| + |.((z - y) . i).|
proof
A5: ( |.((x - y) . i).| = |.((x . i) - (y . i)).| & |.((x - z) . i).| = |.((x . i) - (z . i)).| & |.((z - y) . i).| = |.((z . i) - (y . i)).| ) by A1, RVSUM_1:27;
|.(((x . i) - (z . i)) + ((z . i) - (y . i))).| <= |.((x . i) - (z . i)).| + |.((z . i) - (y . i)).| by COMPLEX1:56;
hence |.((x - y) . i).| <= |.((x - z) . i).| + |.((z - y) . i).| by A5; :: thesis: verum
end;
hence (abs (x - y)) . i <= ((abs (x - z)) . i) + ((abs (z - y)) . i) by A4; :: thesis: verum
end;
((abs (x - z)) . i) + ((abs (z - y)) . i) <= sxz + szy
proof
A6: ( dom (abs (x - z)) = Seg n & dom (abs (z - y)) = Seg n & dom (abs (x - y)) = Seg n ) by FINSEQ_2:124;
( (abs (x - z)) . i in rng (abs (x - z)) & (abs (z - y)) . i in rng (abs (z - y)) ) by A6, A1, FUNCT_1:def 3;
then A7: ( (abs (x - z)) . i <= sup (rng (abs (x - z))) & (abs (z - y)) . i <= sup (rng (abs (z - y))) ) by XXREAL_2:4;
( (abs (x - z)) . i in REAL & (abs (z - y)) . i in REAL ) by A1, A6, Th2;
then ((abs (x - z)) . i) + ((abs (z - y)) . i) <= (sup (rng (abs (x - z)))) + (sup (rng (abs (z - y)))) by Th3, A7;
hence ((abs (x - z)) . i) + ((abs (z - y)) . i) <= sxz + szy by XXREAL_3:def 2; :: thesis: verum
end;
hence (abs (x - y)) . i <= sxz + szy by A3, XXREAL_0:2; :: thesis: verum
end;
hence er <= sxz + szy by A2; :: thesis: verum
end;
then sxz + szy is UpperBound of rng (abs (x - y)) by XXREAL_2:def 1;
hence sxy <= sxz + szy by XXREAL_2:def 3; :: thesis: verum
end;
then sxy <= sxz + ((Infty_dist n) . (z,y)) by Def7;
then sxy <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y)) by Def7;
hence (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (z,y)) by Def7; :: thesis: verum