let M be MetrStruct ; 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; 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 ; ( ( 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 )
( ( 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
;
M is Reflexive
now for a being Element of M holds dist (a,a) = 0 let a be
Element of
M;
dist (a,a) = 0 now dist (a,a) = 0 per cases
( a = A or a <> A )
;
suppose
a <> A
;
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
;
verum end; end; end; hence
dist (
a,
a)
= 0
;
verum end;
hence
M is
Reflexive
by METRIC_1:1;
verum
end;
thus
( 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 A6:
well_dist (
A,
X) is
symmetric
;
M is symmetric
now for a, b being Element of M holds dist (a,b) = dist (b,a)let a,
b be
Element of
M;
dist (a,b) = dist (b,a)now 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 A7:
(
a = A &
b <> A )
;
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;
verum end; suppose A11:
(
a <> A &
b = A )
;
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;
verum end; suppose A15:
(
a <> A &
b <> A )
;
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
;
verum end; end; end; hence
dist (
a,
b)
= dist (
b,
a)
;
verum end;
hence
M is
symmetric
by METRIC_1:3;
verum
end;
thus
( 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 A18:
(
well_dist (
A,
X) is
triangle &
well_dist (
A,
X) is
Reflexive )
;
M is triangle
now 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;
dist (a,c) <= (dist (a,b)) + (dist (b,c))now 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 )
;
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;
verum end; suppose A22:
(
a = A &
b <> A &
c = A )
;
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;
verum end; suppose A27:
(
a = A &
b <> A &
c <> A )
;
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;
verum end; suppose A33:
(
a <> A &
b = A &
c <> A )
;
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;
verum end; suppose A38:
(
a <> A &
b <> A &
c = A )
;
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;
verum end; suppose
(
a <> A &
b <> A &
c <> A )
;
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;
verum end; end; end; hence
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
;
verum end;
hence
M is
triangle
by METRIC_1:4;
verum
end;
assume A45:
( well_dist (A,X) is discerning & well_dist (A,X) is Reflexive )
; M is discerning
now for a, b being Point of M st dist (a,b) = 0 holds
a = blet a,
b be
Point of
M;
( dist (a,b) = 0 implies a = b )assume A46:
dist (
a,
b)
= 0
;
a = bnow a = bper cases
( ( a = A & b = A ) or ( a = A & b <> A ) or ( a <> A & b = A ) or ( a <> A & b <> A ) )
;
suppose A47:
(
a = A &
b <> A )
;
a = bthen 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;
verum end; suppose A49:
(
a <> A &
b = A )
;
a = bthen 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;
verum end; suppose
(
a <> A &
b <> A )
;
a = bthen 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;
verum end; end; end; hence
a = b
;
verum end;
hence
M is discerning
by METRIC_1:2; verum