let X, Y, Z, W be non empty MetrSpace; 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:]; ( (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 iff x = y )
reconsider x1 = x `1_4 , y1 = y `1_4 as Element of X ;
reconsider x2 = x `2_4 , y2 = y `2_4 as Element of Y ;
reconsider x3 = x `3_4 , y3 = y `3_4 as Element of Z ;
reconsider x4 = x `4_4 , y4 = y `4_4 as Element of W ;
A1:
( x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] )
;
thus
( (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 implies x = y )
( x = y implies (dist_cart4 (X,Y,Z,W)) . (x,y) = 0 )proof
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));
A2:
(
0 <= dist (
x3,
y3) &
0 <= dist (
x4,
y4) )
by METRIC_1:5;
then A3:
0 + 0 <= (dist (x3,y3)) + (dist (x4,y4))
by XREAL_1:7;
assume
(dist_cart4 (X,Y,Z,W)) . (
x,
y)
= 0
;
x = y
then A4:
((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) = 0
by A1, Def7;
A5:
(
0 <= dist (
x1,
y1) &
0 <= dist (
x2,
y2) )
by METRIC_1:5;
then A6:
0 + 0 <= (dist (x1,y1)) + (dist (x2,y2))
by XREAL_1:7;
then A7:
(dist (x1,y1)) + (dist (x2,y2)) = 0
by A4, A3, XREAL_1:27;
then
dist (
x2,
y2)
= 0
by A5, XREAL_1:27;
then A8:
x2 = y2
by METRIC_1:2;
A9:
(dist (x3,y3)) + (dist (x4,y4)) = 0
by A4, A6, A3, XREAL_1:27;
then
dist (
x3,
y3)
= 0
by A2, XREAL_1:27;
then A10:
x3 = y3
by METRIC_1:2;
dist (
x4,
y4)
= 0
by A2, A9, XREAL_1:27;
then A11:
x4 = y4
by METRIC_1:2;
dist (
x1,
y1)
= 0
by A5, A7, XREAL_1:27;
hence
x = y
by A1, A8, A10, A11, METRIC_1:2;
verum
end;
assume A12:
x = y
; (dist_cart4 (X,Y,Z,W)) . (x,y) = 0
then A13:
( dist (x2,y2) = 0 & dist (x3,y3) = 0 )
by METRIC_1:1;
A14:
dist (x4,y4) = 0
by A12, 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 A12, A13, A14, METRIC_1:1
;
hence
(dist_cart4 (X,Y,Z,W)) . (x,y) = 0
; verum