let x, y be Element of [:REAL,REAL,REAL:]; ( 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 )
( x = y implies Eukl_dist3 . (x,y) = 0 )proof
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
;
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;
verum
end;
assume A8:
x = y
; 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
; verum