let n be non zero Nat; :: thesis: for x, y being Element of REAL n holds
( (Infty_dist n) . (x,y) = 0 iff x = y )
let x, y be Element of REAL n; :: thesis: ( (Infty_dist n) . (x,y) = 0 iff x = y )
consider S being ext-real-membered set such that
A1: S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } and
A2: (Infty_dist n) . (x,y) = sup S by Th57;
hereby :: thesis: ( x = y implies (Infty_dist n) . (x,y) = 0 )
assume A3: (Infty_dist n) . (x,y) = 0 ; :: thesis: x = y
A4: ( dom x = Seg n & dom y = Seg n ) by FINSEQ_2:124;
now :: thesis: for i being object st i in dom x holds
x . i = y . i
let i be object ; :: thesis: ( i in dom x implies x . i = y . i )
assume A5: i in dom x ; :: thesis: x . i = y . i
then A6: i in Seg n by FINSEQ_2:124;
set AXY = (abs (x - y)) . i;
reconsider f = x - y as complex-valued Function ;
A7: (abs (x - y)) . i = |.((x - y) . i).| by VALUED_1:18;
then A8: 0 <= (abs (x - y)) . i by COMPLEX1:46;
(abs (x - y)) . i = |.((x . i) - (y . i)).| by A5, A7, RVSUM_1:27;
then (abs (x - y)) . i in S by A1, A6;
then (abs (x - y)) . i = 0 by A8, A3, A2, XXREAL_2:4;
then A9: (x - y) . i = 0 by A7, ABSVALUE:2;
reconsider rx = x, ry = y as Element of n -tuples_on REAL ;
(rx - ry) . i = (rx . i) - (ry . i) by A5, RVSUM_1:27;
hence x . i = y . i by A9; :: thesis: verum
end;
hence x = y by A4, FUNCT_1:def 11; :: thesis: verum
end;
assume A10: x = y ; :: thesis: (Infty_dist n) . (x,y) = 0
S = {0}
proof
for t being object st t in S holds
t in {0}
proof
let t be object ; :: thesis: ( t in S implies t in {0} )
assume t in S ; :: thesis: t in {0}
then consider i being Element of Seg n such that
A11: t = |.((x . i) - (y . i)).| by A1;
t = 0 by A11, A10, ABSVALUE:2;
hence t in {0} by TARSKI:def 1; :: thesis: verum
end;
then A12: S c= {0} ;
for t being object st t in {0} holds
t in S
proof
let t be object ; :: thesis: ( t in {0} implies t in S )
assume A13: t in {0} ; :: thesis: t in S
( 1 <= 1 & 1 <= n ) by NAT_1:53;
then 1 is Element of Seg n by FINSEQ_1:1;
then ( |.((x . 1) - (y . 1)).| in S & |.((x . 1) - (y . 1)).| = 0 ) by A10, ABSVALUE:2, A1;
hence t in S by A13, TARSKI:def 1; :: thesis: verum
end;
then {0} c= S ;
hence S = {0} by A12; :: thesis: verum
end;
hence (Infty_dist n) . (x,y) = 0 by A2, XXREAL_2:11; :: thesis: verum