let X, Y be non empty MetrSpace; for x, y being Element of [: the carrier of X, the carrier of Y:] holds
( (dist_cart2 (X,Y)) . (x,y) = 0 iff x = y )
let x, y be Element of [: the carrier of X, the carrier of Y:]; ( (dist_cart2 (X,Y)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , y1 = y `1 as Element of X ;
reconsider x2 = x `2 , y2 = y `2 as Element of Y ;
A1:
( x = [x1,x2] & y = [y1,y2] )
;
thus
( (dist_cart2 (X,Y)) . (x,y) = 0 implies x = y )
( x = y implies (dist_cart2 (X,Y)) . (x,y) = 0 )proof
set d1 =
dist (
x1,
y1);
set d2 =
dist (
x2,
y2);
assume
(dist_cart2 (X,Y)) . (
x,
y)
= 0
;
x = y
then A2:
(dist (x1,y1)) + (dist (x2,y2)) = 0
by A1, Def1;
A3:
(
0 <= dist (
x1,
y1) &
0 <= dist (
x2,
y2) )
by METRIC_1:5;
then
dist (
x1,
y1)
= 0
by A2, XREAL_1:27;
then A4:
x1 = y1
by METRIC_1:2;
dist (
x2,
y2)
= 0
by A2, A3, XREAL_1:27;
hence
x = y
by A1, A4, METRIC_1:2;
verum
end;
assume A5:
x = y
; (dist_cart2 (X,Y)) . (x,y) = 0
then A6:
dist (x2,y2) = 0
by METRIC_1:1;
(dist_cart2 (X,Y)) . (x,y) =
(dist (x1,y1)) + (dist (x2,y2))
by A1, Def1
.=
0
by A5, A6, METRIC_1:1
;
hence
(dist_cart2 (X,Y)) . (x,y) = 0
; verum