let x, y be Element of [:REAL,REAL,REAL:]; :: thesis: ( Eukl_dist3 . (x,y) = 0 iff x = y )

reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;

A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ;

thus ( Eukl_dist3 . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies Eukl_dist3 . (x,y) = 0 )

then A9: ( (real_dist . (x1,y1)) ^2 = 0 ^2 & (real_dist . (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:8;

Eukl_dist3 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by A1, Def22

.= 0 ^2 by A8, A9, METRIC_1:8, SQUARE_1:17 ;

hence Eukl_dist3 . (x,y) = 0 ; :: thesis: verum

reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;

A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ;

thus ( Eukl_dist3 . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies Eukl_dist3 . (x,y) = 0 )

proof

assume A8:
x = y
; :: thesis: Eukl_dist3 . (x,y) = 0
set d3 = real_dist . (x3,y3);

set d2 = real_dist . (x2,y2);

set d1 = real_dist . (x1,y1);

A2: ( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;

assume Eukl_dist3 . (x,y) = 0 ; :: thesis: x = y

then sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) = 0 by A1, Def22;

then A3: sqrt (((real_dist . (x1,y1)) ^2) + (((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2))) = 0 ;

( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;

then A4: ( 0 <= (real_dist . (x1,y1)) ^2 & 0 + 0 <= ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) ) by XREAL_1:7, XREAL_1:63;

then real_dist . (x1,y1) = 0 by A3, Lm1;

then A5: x1 = y1 by METRIC_1:8;

A6: ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) = 0 by A3, A4, Lm1;

then real_dist . (x2,y2) = 0 by A2, XREAL_1:27;

then A7: x2 = y2 by METRIC_1:8;

real_dist . (x3,y3) = 0 by A6, A2, XREAL_1:27;

hence x = y by A1, A5, A7, METRIC_1:8; :: thesis: verum

end;set d2 = real_dist . (x2,y2);

set d1 = real_dist . (x1,y1);

A2: ( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;

assume Eukl_dist3 . (x,y) = 0 ; :: thesis: x = y

then sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) = 0 by A1, Def22;

then A3: sqrt (((real_dist . (x1,y1)) ^2) + (((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2))) = 0 ;

( 0 <= (real_dist . (x2,y2)) ^2 & 0 <= (real_dist . (x3,y3)) ^2 ) by XREAL_1:63;

then A4: ( 0 <= (real_dist . (x1,y1)) ^2 & 0 + 0 <= ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) ) by XREAL_1:7, XREAL_1:63;

then real_dist . (x1,y1) = 0 by A3, Lm1;

then A5: x1 = y1 by METRIC_1:8;

A6: ((real_dist . (x2,y2)) ^2) + ((real_dist . (x3,y3)) ^2) = 0 by A3, A4, Lm1;

then real_dist . (x2,y2) = 0 by A2, XREAL_1:27;

then A7: x2 = y2 by METRIC_1:8;

real_dist . (x3,y3) = 0 by A6, A2, XREAL_1:27;

hence x = y by A1, A5, A7, METRIC_1:8; :: thesis: verum

then A9: ( (real_dist . (x1,y1)) ^2 = 0 ^2 & (real_dist . (x2,y2)) ^2 = 0 ^2 ) by METRIC_1:8;

Eukl_dist3 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by A1, Def22

.= 0 ^2 by A8, A9, METRIC_1:8, SQUARE_1:17 ;

hence Eukl_dist3 . (x,y) = 0 ; :: thesis: verum