let M be MetrStruct ; :: thesis: for a being Point of M
for X being set holds
( ( M is Reflexive implies WellSpace (a,X) is Reflexive ) & ( M is symmetric implies WellSpace (a,X) is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )
let a be Point of M; :: thesis: for X being set holds
( ( M is Reflexive implies WellSpace (a,X) is Reflexive ) & ( M is symmetric implies WellSpace (a,X) is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )
let X be set ; :: thesis: ( ( M is Reflexive implies WellSpace (a,X) is Reflexive ) & ( M is symmetric implies WellSpace (a,X) is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )
set XX = [:X,( the carrier of M \ {a}):] \/ {[X,a]};
set w = well_dist (a,X);
set W = WellSpace (a,X);
thus ( M is Reflexive implies WellSpace (a,X) is Reflexive ) :: thesis: ( ( M is symmetric implies WellSpace (a,X) is symmetric ) & ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )
proof
assume A1: M is Reflexive ; :: thesis: WellSpace (a,X) is Reflexive
now :: thesis: for A being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]} holds (well_dist (a,X)) . (A,A) = 0
let A be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist (a,X)) . (A,A) = 0
consider y being set , b being Point of M such that
A2: A = [y,b] and
( ( y in X & b <> a ) or ( y = X & b = a ) ) by Th37;
thus (well_dist (a,X)) . (A,A) = dist (b,b) by A2, Def10
.= 0 by A1, METRIC_1:1 ; :: thesis: verum
end;
then well_dist (a,X) is Reflexive ;
hence WellSpace (a,X) is Reflexive ; :: thesis: verum
end;
thus ( M is symmetric implies WellSpace (a,X) is symmetric ) :: thesis: ( ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) & ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning ) )
proof
assume M is symmetric ; :: thesis: WellSpace (a,X) is symmetric
then reconsider M = M as symmetric MetrStruct ;
reconsider a = a as Point of M ;
now :: thesis: for A, B being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]} holds (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
let A, B be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
consider y1 being set , b1 being Point of M such that
A3: A = [y1,b1] and
A4: ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th37;
consider y2 being set , b2 being Point of M such that
A5: B = [y2,b2] and
A6: ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th37;
now :: thesis: (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
per cases ( ( b1 = a & y1 = X & b2 = a & y2 = X ) or y1 <> y2 or ( b1 <> a & b2 <> a & y1 = y2 ) ) by A4, A6;
suppose ( b1 = a & y1 = X & b2 = a & y2 = X ) ; :: thesis: (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
hence (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A) by A3, A5; :: thesis: verum
end;
suppose A7: y1 <> y2 ; :: thesis: (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
hence (well_dist (a,X)) . (A,B) = (dist (b1,a)) + (dist (a,b2)) by A3, A5, Def10
.= (dist (a,b1)) + (dist (a,b2))
.= (dist (a,b1)) + (dist (b2,a))
.= (well_dist (a,X)) . (B,A) by A3, A5, A7, Def10 ;
:: thesis: verum
end;
suppose A8: ( b1 <> a & b2 <> a & y1 = y2 ) ; :: thesis: (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A)
hence (well_dist (a,X)) . (A,B) = dist (b1,b2) by A3, A5, Def10
.= dist (b2,b1)
.= (well_dist (a,X)) . (B,A) by A3, A5, A8, Def10 ;
:: thesis: verum
end;
end;
end;
hence (well_dist (a,X)) . (A,B) = (well_dist (a,X)) . (B,A) ; :: thesis: verum
end;
then well_dist (a,X) is symmetric ;
hence WellSpace (a,X) is symmetric ; :: thesis: verum
end;
thus ( M is triangle & M is symmetric & M is Reflexive implies WellSpace (a,X) is triangle ) :: thesis: ( M is triangle & M is symmetric & M is Reflexive & M is discerning implies WellSpace (a,X) is discerning )
proof
assume A9: ( M is triangle & M is symmetric & M is Reflexive ) ; :: thesis: WellSpace (a,X) is triangle
now :: thesis: for A, B, C being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]} holds (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
let A, B, C be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
consider y1 being set , b1 being Point of M such that
A10: A = [y1,b1] and
( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th37;
consider y2 being set , b2 being Point of M such that
A11: B = [y2,b2] and
( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th37;
consider y3 being set , b3 being Point of M such that
A12: C = [y3,b3] and
( ( y3 in X & b3 <> a ) or ( y3 = X & b3 = a ) ) by Th37;
now :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
per cases ( ( y1 = y2 & y1 = y3 ) or ( y1 <> y2 & y1 = y3 ) or ( y1 = y2 & y1 <> y3 ) or ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) or ( y1 <> y2 & y1 <> y3 & y2 = y3 ) ) ;
suppose A13: ( y1 = y2 & y1 = y3 ) ; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
then A14: dist (b2,b3) = (well_dist (a,X)) . (B,C) by A11, A12, Def10;
A15: dist (b1,b2) = (well_dist (a,X)) . (A,B) by A10, A11, A13, Def10;
dist (b1,b3) = (well_dist (a,X)) . (A,C) by A10, A12, A13, Def10;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A9, A15, A14, METRIC_1:4; :: thesis: verum
end;
suppose A16: ( y1 <> y2 & y1 = y3 ) ; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
then A17: (dist (b2,a)) + (dist (a,b3)) = (well_dist (a,X)) . (B,C) by A11, A12, Def10;
A18: dist (b1,b2) <= (dist (b1,a)) + (dist (a,b2)) by A9, METRIC_1:4;
A19: dist (b2,b3) <= (dist (b2,a)) + (dist (a,b3)) by A9, METRIC_1:4;
(dist (b1,a)) + (dist (a,b2)) = (well_dist (a,X)) . (A,B) by A10, A11, A16, Def10;
then A20: (dist (b1,b2)) + (dist (b2,b3)) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A17, A18, A19, XREAL_1:7;
A21: dist (b1,b3) <= (dist (b1,b2)) + (dist (b2,b3)) by A9, METRIC_1:4;
dist (b1,b3) = (well_dist (a,X)) . (A,C) by A10, A12, A16, Def10;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A20, A21, XXREAL_0:2; :: thesis: verum
end;
suppose A22: ( y1 = y2 & y1 <> y3 ) ; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
A23: dist (b1,a) <= (dist (b1,b2)) + (dist (b2,a)) by A9, METRIC_1:4;
(dist (b1,a)) + (dist (a,b3)) = (well_dist (a,X)) . (A,C) by A10, A12, A22, Def10;
then A24: (well_dist (a,X)) . (A,C) <= ((dist (b1,b2)) + (dist (b2,a))) + (dist (a,b3)) by A23, XREAL_1:6;
A25: (dist (b2,a)) + (dist (a,b3)) = (well_dist (a,X)) . (B,C) by A11, A12, A22, Def10;
dist (b1,b2) = (well_dist (a,X)) . (A,B) by A10, A11, A22, Def10;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A25, A24; :: thesis: verum
end;
suppose A26: ( y1 <> y2 & y1 <> y3 & y2 <> y3 ) ; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
A27: 0 <= dist (b2,a) by A9, METRIC_1:5;
(dist (b2,a)) + (dist (a,b3)) = (well_dist (a,X)) . (B,C) by A11, A12, A26, Def10;
then A28: 0 + (dist (a,b3)) <= (well_dist (a,X)) . (B,C) by A27, XREAL_1:6;
A29: 0 <= dist (a,b2) by A9, METRIC_1:5;
(dist (b1,a)) + (dist (a,b2)) = (well_dist (a,X)) . (A,B) by A10, A11, A26, Def10;
then A30: (dist (b1,a)) + 0 <= (well_dist (a,X)) . (A,B) by A29, XREAL_1:6;
(dist (b1,a)) + (dist (a,b3)) = (well_dist (a,X)) . (A,C) by A10, A12, A26, Def10;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A30, A28, XREAL_1:7; :: thesis: verum
end;
suppose A31: ( y1 <> y2 & y1 <> y3 & y2 = y3 ) ; :: thesis: (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C))
A32: dist (a,b3) <= (dist (a,b2)) + (dist (b2,b3)) by A9, METRIC_1:4;
(dist (b1,a)) + (dist (a,b3)) = (well_dist (a,X)) . (A,C) by A10, A12, A31, Def10;
then A33: (well_dist (a,X)) . (A,C) <= (dist (b1,a)) + ((dist (a,b2)) + (dist (b2,b3))) by A32, XREAL_1:7;
A34: dist (b2,b3) = (well_dist (a,X)) . (B,C) by A11, A12, A31, Def10;
(dist (b1,a)) + (dist (a,b2)) = (well_dist (a,X)) . (A,B) by A10, A11, A31, Def10;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) by A34, A33; :: thesis: verum
end;
end;
end;
hence (well_dist (a,X)) . (A,C) <= ((well_dist (a,X)) . (A,B)) + ((well_dist (a,X)) . (B,C)) ; :: thesis: verum
end;
then well_dist (a,X) is triangle ;
hence WellSpace (a,X) is triangle ; :: thesis: verum
end;
assume A35: ( M is triangle & M is symmetric & M is Reflexive & M is discerning ) ; :: thesis: WellSpace (a,X) is discerning
now :: thesis: for A, B being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]} st (well_dist (a,X)) . (A,B) = 0 holds
A = B
let A, B be Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}; :: thesis: ( (well_dist (a,X)) . (A,B) = 0 implies A = B )
consider y1 being set , b1 being Point of M such that
A36: A = [y1,b1] and
A37: ( ( y1 in X & b1 <> a ) or ( y1 = X & b1 = a ) ) by Th37;
consider y2 being set , b2 being Point of M such that
A38: B = [y2,b2] and
A39: ( ( y2 in X & b2 <> a ) or ( y2 = X & b2 = a ) ) by Th37;
assume A40: (well_dist (a,X)) . (A,B) = 0 ; :: thesis: A = B
now :: thesis: A = B
per cases ( y1 = y2 or y1 <> y2 ) ;
suppose A41: y1 = y2 ; :: thesis: A = B
then (well_dist (a,X)) . (A,B) = dist (b1,b2) by A36, A38, Def10;
hence A = B by A35, A40, A36, A38, A41, METRIC_1:2; :: thesis: verum
end;
suppose y1 <> y2 ; :: thesis: A = B
then A42: (well_dist (a,X)) . (A,B) = (dist (b1,a)) + (dist (a,b2)) by A36, A38, Def10;
A43: dist (b1,a) >= 0 by A35, METRIC_1:5;
dist (a,b2) >= 0 by A35, METRIC_1:5;
then dist (b1,a) = 0 by A40, A42, A43;
hence A = B by A35, A40, A36, A37, A38, A39, A42, METRIC_1:2; :: thesis: verum
end;
end;
end;
hence A = B ; :: thesis: verum
end;
then well_dist (a,X) is discerning ;
hence WellSpace (a,X) is discerning ; :: thesis: verum