let X, Y, Z be non empty MetrSpace; for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z:] holds
( (dist_cart3S X,Y,Z) . x,y = 0 iff x = y )
let x, y be Element of [:the carrier of X,the carrier of Y,the carrier of Z:]; ( (dist_cart3S X,Y,Z) . 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 ;
reconsider x3 = x `3 , y3 = y `3 as Element of Z ;
A1:
( x = [x1,x2,x3] & y = [y1,y2,y3] )
by MCART_1:48;
thus
( (dist_cart3S X,Y,Z) . x,y = 0 implies x = y )
( x = y implies (dist_cart3S X,Y,Z) . x,y = 0 )proof
set d3 =
dist x3,
y3;
set d2 =
dist x2,
y2;
set d1 =
dist x1,
y1;
A2:
(
0 <= (dist x2,y2) ^2 &
0 <= (dist x3,y3) ^2 )
by XREAL_1:65;
assume
(dist_cart3S X,Y,Z) . x,
y = 0
;
x = y
then
sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 )) = 0
by A1, Def4;
then A3:
sqrt (((dist x1,y1) ^2 ) + (((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ))) = 0
;
(
0 <= (dist x2,y2) ^2 &
0 <= (dist x3,y3) ^2 )
by XREAL_1:65;
then A4:
(
0 <= (dist x1,y1) ^2 &
0 + 0 <= ((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ) )
by XREAL_1:9, XREAL_1:65;
then
dist x1,
y1 = 0
by A3, Th2;
then A5:
x1 = y1
by METRIC_1:2;
A6:
((dist x2,y2) ^2 ) + ((dist x3,y3) ^2 ) = 0
by A3, A4, Th2;
then
dist x2,
y2 = 0
by A2, XREAL_1:29;
then A7:
x2 = y2
by METRIC_1:2;
dist x3,
y3 = 0
by A6, A2, XREAL_1:29;
hence
x = y
by A1, A5, A7, METRIC_1:2;
verum
end;
assume A8:
x = y
; (dist_cart3S X,Y,Z) . x,y = 0
then A9:
( (dist x1,y1) ^2 = 0 ^2 & (dist x2,y2) ^2 = 0 ^2 )
by METRIC_1:1;
(dist_cart3S X,Y,Z) . x,y =
sqrt ((((dist x1,y1) ^2 ) + ((dist x2,y2) ^2 )) + ((dist x3,y3) ^2 ))
by A1, Def4
.=
0 ^2
by A8, A9, METRIC_1:1, SQUARE_1:82
;
hence
(dist_cart3S X,Y,Z) . x,y = 0
; verum