let X, Y, Z, W be non empty MetrSpace; :: thesis: for x, y being Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:] holds
( (dist_cart4 X,Y,Z,W) . x,y = 0 iff x = y )
let x, y be Element of [:the carrier of X,the carrier of Y,the carrier of Z,the carrier of W:]; :: thesis: ( (dist_cart4 X,Y,Z,W) . 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 ;
reconsider x4 = x `4 , y4 = y `4 as Element of W ;
A1:
( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] )
by MCART_1:60;
thus
( (dist_cart4 X,Y,Z,W) . x,y = 0 implies x = y )
:: thesis: ( x = y implies (dist_cart4 X,Y,Z,W) . x,y = 0 )proof
assume A2:
(dist_cart4 X,Y,Z,W) . x,
y = 0
;
:: thesis: x = y
set d1 =
dist x1,
y1;
set d2 =
dist x2,
y2;
set d3 =
dist x3,
y3;
set d5 =
dist x4,
y4;
set d4 =
(dist x1,y1) + (dist x2,y2);
set d6 =
(dist x3,y3) + (dist x4,y4);
A3:
((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4)) = 0
by A1, A2, Def7;
A4:
(
0 <= dist x1,
y1 &
0 <= dist x2,
y2 )
by METRIC_1:5;
then A5:
0 + 0 <= (dist x1,y1) + (dist x2,y2)
by XREAL_1:9;
A6:
(
0 <= dist x3,
y3 &
0 <= dist x4,
y4 )
by METRIC_1:5;
then
0 + 0 <= (dist x3,y3) + (dist x4,y4)
by XREAL_1:9;
then A7:
(
(dist x1,y1) + (dist x2,y2) = 0 &
(dist x3,y3) + (dist x4,y4) = 0 )
by A3, A5, XREAL_1:29;
then A8:
(
dist x1,
y1 = 0 &
dist x2,
y2 = 0 )
by A4, XREAL_1:29;
then A9:
x2 = y2
by METRIC_1:2;
(
dist x3,
y3 = 0 &
dist x4,
y4 = 0 )
by A6, A7, XREAL_1:29;
then
(
x3 = y3 &
x4 = y4 )
by METRIC_1:2;
hence
x = y
by A1, A8, A9, METRIC_1:2;
:: thesis: verum
end;
assume A10:
x = y
; :: thesis: (dist_cart4 X,Y,Z,W) . x,y = 0
then A11:
dist x2,y2 = 0
by METRIC_1:1;
A12:
( dist x3,y3 = 0 & dist x4,y4 = 0 )
by A10, METRIC_1:1;
(dist_cart4 X,Y,Z,W) . x,y =
((dist x1,y1) + (dist x2,y2)) + ((dist x3,y3) + (dist x4,y4))
by A1, Def7
.=
0
by A10, A11, A12, METRIC_1:1
;
hence
(dist_cart4 X,Y,Z,W) . x,y = 0
; :: thesis: verum