let x, y be Element of [:REAL,REAL:]; ( taxi_dist2 . (x,y) = 0 iff x = y )
reconsider x1 = x `1 , x2 = x `2 , y1 = y `1 , y2 = y `2 as Element of REAL ;
A1:
( x = [x1,x2] & y = [y1,y2] )
;
thus
( taxi_dist2 . (x,y) = 0 implies x = y )
( x = y implies taxi_dist2 . (x,y) = 0 )proof
set d2 =
real_dist . (
x2,
y2);
set d1 =
real_dist . (
x1,
y1);
real_dist . (
x1,
y1)
= |.(x1 - y1).|
by METRIC_1:def 12;
then A2:
0 <= real_dist . (
x1,
y1)
by COMPLEX1:46;
real_dist . (
x2,
y2)
= |.(x2 - y2).|
by METRIC_1:def 12;
then A3:
0 <= real_dist . (
x2,
y2)
by COMPLEX1:46;
assume
taxi_dist2 . (
x,
y)
= 0
;
x = y
then A4:
(real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0
by A1, Def16;
then
real_dist . (
x1,
y1)
= 0
by A2, A3, XREAL_1:27;
then A5:
x1 = y1
by METRIC_1:8;
real_dist . (
x2,
y2)
= 0
by A4, A2, A3, XREAL_1:27;
hence
x = y
by A1, A5, METRIC_1:8;
verum
end;
assume A6:
x = y
; taxi_dist2 . (x,y) = 0
then A7:
real_dist . (x2,y2) = 0
by METRIC_1:8;
taxi_dist2 . (x,y) =
(real_dist . (x1,y1)) + (real_dist . (x2,y2))
by A1, Def16
.=
0
by A6, A7, METRIC_1:8
;
hence
taxi_dist2 . (x,y) = 0
; verum