let M be MetrStruct ; :: thesis: for a being Point of M
for X being non empty set holds
( ( well_dist (a,X) is Reflexive implies M is Reflexive ) & ( well_dist (a,X) is symmetric implies M is symmetric ) & ( well_dist (a,X) is triangle & well_dist (a,X) is Reflexive implies M is triangle ) & ( well_dist (a,X) is discerning & well_dist (a,X) is Reflexive implies M is discerning ) )
let A be Point of M; :: thesis: for X being non empty set holds
( ( well_dist (A,X) is Reflexive implies M is Reflexive ) & ( well_dist (A,X) is symmetric implies M is symmetric ) & ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive implies M is triangle ) & ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive implies M is discerning ) )
let X be non empty set ; :: thesis: ( ( well_dist (A,X) is Reflexive implies M is Reflexive ) & ( well_dist (A,X) is symmetric implies M is symmetric ) & ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive implies M is triangle ) & ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive implies M is discerning ) )
consider x0 being object such that
A1: x0 in X by XBOOLE_0:def 1;
set w = well_dist (A,X);
set XX = [:X,( the carrier of M \ {A}):] \/ {[X,A]};
thus A2: ( well_dist (A,X) is Reflexive implies M is Reflexive ) :: thesis: ( ( well_dist (A,X) is symmetric implies M is symmetric ) & ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive implies M is triangle ) & ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive implies M is discerning ) )
proof
assume A3: well_dist (A,X) is Reflexive ; :: thesis: M is Reflexive
now :: thesis: for a being Element of M holds dist (a,a) = 0
let a be Element of M; :: thesis: dist (a,a) = 0
now :: thesis: dist (a,a) = 0
per cases ( a = A or a <> A ) ;
suppose a = A ; :: thesis: dist (a,a) = 0
then A4: [X,a] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by Th37;
hence dist (a,a) = (well_dist (A,X)) . ([X,a],[X,a]) by Def10
.= 0 by A3, A4 ;
:: thesis: verum
end;
suppose a <> A ; :: thesis: dist (a,a) = 0
then A5: [x0,a] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
hence dist (a,a) = (well_dist (A,X)) . ([x0,a],[x0,a]) by Def10
.= 0 by A3, A5 ;
:: thesis: verum
end;
end;
end;
hence dist (a,a) = 0 ; :: thesis: verum
end;
hence M is Reflexive by METRIC_1:1; :: thesis: verum
end;
thus ( well_dist (A,X) is symmetric implies M is symmetric ) :: thesis: ( ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive implies M is triangle ) & ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive implies M is discerning ) )
proof
assume A6: well_dist (A,X) is symmetric ; :: thesis: M is symmetric
now :: thesis: for a, b being Element of M holds dist (a,b) = dist (b,a)
let a, b be Element of M; :: thesis: dist (a,b) = dist (b,a)
now :: thesis: dist (a,b) = dist (b,a)
per cases ( ( a = A & b = A ) or ( a = A & b <> A ) or ( a <> A & b = A ) or ( a <> A & b <> A ) ) ;
suppose ( a = A & b = A ) ; :: thesis: dist (a,b) = dist (b,a)
hence dist (a,b) = dist (b,a) ; :: thesis: verum
end;
suppose A7: ( a = A & b <> A ) ; :: thesis: dist (a,b) = dist (b,a)
then A8: [x0,b] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
A9: [X,A] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A10: X <> x0 by A1;
then (dist (A,A)) + (dist (A,b)) = (well_dist (A,X)) . ([X,A],[x0,b]) by A9, A8, Def10
.= (well_dist (A,X)) . ([x0,b],[X,A]) by A6, A9, A8
.= (dist (b,A)) + (dist (A,A)) by A9, A8, A10, Def10 ;
hence dist (a,b) = dist (b,a) by A7; :: thesis: verum
end;
suppose A11: ( a <> A & b = A ) ; :: thesis: dist (a,b) = dist (b,a)
then A12: [x0,a] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
A13: [X,A] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A14: X <> x0 by A1;
then (dist (A,A)) + (dist (A,a)) = (well_dist (A,X)) . ([X,A],[x0,a]) by A13, A12, Def10
.= (well_dist (A,X)) . ([x0,a],[X,A]) by A6, A13, A12
.= (dist (a,A)) + (dist (A,A)) by A13, A12, A14, Def10 ;
hence dist (a,b) = dist (b,a) by A11; :: thesis: verum
end;
suppose A15: ( a <> A & b <> A ) ; :: thesis: dist (a,b) = dist (b,a)
then A16: [x0,b] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
A17: [x0,a] in [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, A15, Th37;
hence dist (a,b) = (well_dist (A,X)) . ([x0,a],[x0,b]) by A16, Def10
.= (well_dist (A,X)) . ([x0,b],[x0,a]) by A6, A17, A16
.= dist (b,a) by A17, A16, Def10 ;
:: thesis: verum
end;
end;
end;
hence dist (a,b) = dist (b,a) ; :: thesis: verum
end;
hence M is symmetric by METRIC_1:3; :: thesis: verum
end;
thus ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive implies M is triangle ) :: thesis: ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive implies M is discerning )
proof
assume A18: ( well_dist (A,X) is triangle & well_dist (A,X) is Reflexive ) ; :: thesis: M is triangle
now :: thesis: for a, b, c being Point of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c))
let a, b, c be Point of M; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
now :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
per cases ( ( a = A & b = A & c = A ) or ( a = A & b = A & c <> A ) or ( a = A & b <> A & c = A ) or ( a = A & b <> A & c <> A ) or ( a <> A & b = A & c = A ) or ( a <> A & b = A & c <> A ) or ( a <> A & b <> A & c = A ) or ( a <> A & b <> A & c <> A ) ) ;
suppose ( a = A & b = A & c = A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [X,a], Xb = [X,b], Xc = [X,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by Th37;
A19: dist (a,c) = (well_dist (A,X)) . (Xa,Xc) by Def10;
A20: dist (a,b) = (well_dist (A,X)) . (Xa,Xb) by Def10;
(well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A19, A20, Def10; :: thesis: verum
end;
suppose A21: ( a = A & b = A & c <> A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
dist (a,a) = 0 by A2, A18, METRIC_1:1;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A21; :: thesis: verum
end;
suppose A22: ( a = A & b <> A & c = A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [X,a], Xb = [x0,b], Xc = [X,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A23: x0 <> X by A1;
then A24: (dist (b,c)) + (dist (a,a)) = (well_dist (A,X)) . (Xb,Xc) by A22, Def10;
A25: dist (a,a) = 0 by A2, A18, METRIC_1:1;
A26: (well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
(dist (a,a)) + (dist (a,b)) = (well_dist (A,X)) . (Xa,Xb) by A22, A23, Def10;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A26, A24, A25, Def10; :: thesis: verum
end;
suppose A27: ( a = A & b <> A & c <> A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [X,a], Xb = [x0,b], Xc = [x0,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A28: x0 <> X by A1;
then A29: (dist (a,a)) + (dist (a,b)) = (well_dist (A,X)) . (Xa,Xb) by A27, Def10;
A30: dist (a,a) = 0 by A2, A18, METRIC_1:1;
A31: (well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
(dist (a,a)) + (dist (a,c)) = (well_dist (A,X)) . (Xa,Xc) by A27, A28, Def10;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A31, A29, A30, Def10; :: thesis: verum
end;
suppose A32: ( a <> A & b = A & c = A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
dist (c,c) = 0 by A2, A18, METRIC_1:1;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A32; :: thesis: verum
end;
suppose A33: ( a <> A & b = A & c <> A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [x0,a], Xb = [X,b], Xc = [x0,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A34: x0 <> X by A1;
then A35: (dist (b,b)) + (dist (b,c)) = (well_dist (A,X)) . (Xb,Xc) by A33, Def10;
A36: dist (b,b) = 0 by A2, A18, METRIC_1:1;
A37: (well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
(dist (a,b)) + (dist (b,b)) = (well_dist (A,X)) . (Xa,Xb) by A33, A34, Def10;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A37, A35, A36, Def10; :: thesis: verum
end;
suppose A38: ( a <> A & b <> A & c = A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [x0,a], Xb = [x0,b], Xc = [X,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then A39: x0 <> X by A1;
then A40: (dist (b,c)) + (dist (c,c)) = (well_dist (A,X)) . (Xb,Xc) by A38, Def10;
A41: dist (c,c) = 0 by A2, A18, METRIC_1:1;
A42: (well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
(dist (a,c)) + (dist (c,c)) = (well_dist (A,X)) . (Xa,Xc) by A38, A39, Def10;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A42, A40, A41, Def10; :: thesis: verum
end;
suppose ( a <> A & b <> A & c <> A ) ; :: thesis: dist (a,c) <= (dist (a,b)) + (dist (b,c))
then reconsider Xa = [x0,a], Xb = [x0,b], Xc = [x0,c] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
A43: dist (a,c) = (well_dist (A,X)) . (Xa,Xc) by Def10;
A44: dist (a,b) = (well_dist (A,X)) . (Xa,Xb) by Def10;
(well_dist (A,X)) . (Xa,Xc) <= ((well_dist (A,X)) . (Xa,Xb)) + ((well_dist (A,X)) . (Xb,Xc)) by A18;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) by A43, A44, Def10; :: thesis: verum
end;
end;
end;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) ; :: thesis: verum
end;
hence M is triangle by METRIC_1:4; :: thesis: verum
end;
assume A45: ( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive ) ; :: thesis: M is discerning
now :: thesis: for a, b being Point of M st dist (a,b) = 0 holds
a = b
let a, b be Point of M; :: thesis: ( dist (a,b) = 0 implies a = b )
assume A46: dist (a,b) = 0 ; :: thesis: a = b
now :: thesis: a = b
per cases ( ( a = A & b = A ) or ( a = A & b <> A ) or ( a <> A & b = A ) or ( a <> A & b <> A ) ) ;
suppose ( a = A & b = A ) ; :: thesis: a = b
hence a = b ; :: thesis: verum
end;
suppose A47: ( a = A & b <> A ) ; :: thesis: a = b
then reconsider Xa = [X,a], Xb = [x0,b] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then x0 <> X by A1;
then A48: (dist (a,a)) + (dist (a,b)) = (well_dist (A,X)) . (Xa,Xb) by A47, Def10;
dist (a,a) = 0 by A2, A45, METRIC_1:1;
then Xa = Xb by A45, A46, A48;
hence a = b by XTUPLE_0:1; :: thesis: verum
end;
suppose A49: ( a <> A & b = A ) ; :: thesis: a = b
then reconsider Xa = [x0,a], Xb = [X,b] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
reconsider xx = x0 as set by TARSKI:1;
not xx in xx ;
then x0 <> X by A1;
then A50: (dist (a,b)) + (dist (b,b)) = (well_dist (A,X)) . (Xa,Xb) by A49, Def10;
dist (b,b) = 0 by A2, A45, METRIC_1:1;
then Xa = Xb by A45, A46, A50;
hence a = b by XTUPLE_0:1; :: thesis: verum
end;
suppose ( a <> A & b <> A ) ; :: thesis: a = b
then reconsider Xa = [x0,a], Xb = [x0,b] as Element of [:X,( the carrier of M \ {A}):] \/ {[X,A]} by A1, Th37;
dist (a,b) = (well_dist (A,X)) . (Xa,Xb) by Def10;
then Xa = Xb by A45, A46;
hence a = b by XTUPLE_0:1; :: thesis: verum
end;
end;
end;
hence a = b ; :: thesis: verum
end;
hence M is discerning by METRIC_1:2; :: thesis: verum