let x, y be Element of [:REAL,REAL,REAL:]; :: thesis: ( taxi_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 ( taxi_dist3 . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies taxi_dist3 . (x,y) = 0 )

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

taxi_dist3 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by A1, Def20

.= 0 by A10, A11, METRIC_1:8 ;

hence taxi_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 ( taxi_dist3 . (x,y) = 0 implies x = y ) :: thesis: ( x = y implies taxi_dist3 . (x,y) = 0 )

proof

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

set d2 = real_dist . (x2,y2);

set d1 = real_dist . (x1,y1);

set d4 = (real_dist . (x1,y1)) + (real_dist . (x2,y2));

real_dist . (x3,y3) = |.(x3 - y3).| by METRIC_1:def 12;

then A2: 0 <= real_dist . (x3,y3) by COMPLEX1:46;

real_dist . (x1,y1) = |.(x1 - y1).| by METRIC_1:def 12;

then A3: 0 <= real_dist . (x1,y1) by COMPLEX1:46;

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

then A4: ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) = 0 by A1, Def20;

real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;

then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;

then A6: 0 + 0 <= (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A3, XREAL_1:7;

then A7: (real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0 by A4, A2, XREAL_1:27;

then real_dist . (x1,y1) = 0 by A5, A3, XREAL_1:27;

then A8: x1 = y1 by METRIC_1:8;

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

then A9: x3 = y3 by METRIC_1:8;

real_dist . (x2,y2) = 0 by A5, A3, A7, XREAL_1:27;

hence x = y by A1, A9, A8, METRIC_1:8; :: thesis: verum

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

set d1 = real_dist . (x1,y1);

set d4 = (real_dist . (x1,y1)) + (real_dist . (x2,y2));

real_dist . (x3,y3) = |.(x3 - y3).| by METRIC_1:def 12;

then A2: 0 <= real_dist . (x3,y3) by COMPLEX1:46;

real_dist . (x1,y1) = |.(x1 - y1).| by METRIC_1:def 12;

then A3: 0 <= real_dist . (x1,y1) by COMPLEX1:46;

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

then A4: ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) = 0 by A1, Def20;

real_dist . (x2,y2) = |.(x2 - y2).| by METRIC_1:def 12;

then A5: 0 <= real_dist . (x2,y2) by COMPLEX1:46;

then A6: 0 + 0 <= (real_dist . (x1,y1)) + (real_dist . (x2,y2)) by A3, XREAL_1:7;

then A7: (real_dist . (x1,y1)) + (real_dist . (x2,y2)) = 0 by A4, A2, XREAL_1:27;

then real_dist . (x1,y1) = 0 by A5, A3, XREAL_1:27;

then A8: x1 = y1 by METRIC_1:8;

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

then A9: x3 = y3 by METRIC_1:8;

real_dist . (x2,y2) = 0 by A5, A3, A7, XREAL_1:27;

hence x = y by A1, A9, A8, METRIC_1:8; :: thesis: verum

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

taxi_dist3 . (x,y) = ((real_dist . (x1,y1)) + (real_dist . (x2,y2))) + (real_dist . (x3,y3)) by A1, Def20

.= 0 by A10, A11, METRIC_1:8 ;

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