let D be set ; for f being Function of [:D,D:],REAL holds
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
let f be Function of [:D,D:],REAL; ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
set DF = MetrStruct(# D,f #);
A1:
( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )
proof
assume
MetrStruct(#
D,
f #) is
MetrSpace
;
f is_metric_of D
then reconsider DF =
MetrStruct(#
D,
f #) as
MetrSpace ;
for
a,
b,
c being
Element of
DF holds
( ( the
distance of
DF . (
a,
b)
= 0 implies
a = b ) & (
a = b implies the
distance of
DF . (
a,
b)
= 0 ) & the
distance of
DF . (
a,
b)
= the
distance of
DF . (
b,
a) & the
distance of
DF . (
a,
c)
<= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
proof
let a,
b,
c be
Element of
DF;
( ( the distance of DF . (a,b) = 0 implies a = b ) & ( a = b implies the distance of DF . (a,b) = 0 ) & the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
A2:
the
distance of
DF . (
a,
b)
= dist (
a,
b)
by METRIC_1:def 1;
hence
( the
distance of
DF . (
a,
b)
= 0 iff
a = b )
by METRIC_1:1, METRIC_1:2;
( the distance of DF . (a,b) = the distance of DF . (b,a) & the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c)) )
the
distance of
DF . (
b,
a)
= dist (
b,
a)
by METRIC_1:def 1;
hence
the
distance of
DF . (
a,
b)
= the
distance of
DF . (
b,
a)
by A2;
the distance of DF . (a,c) <= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c))
( the
distance of
DF . (
a,
c)
= dist (
a,
c) & the
distance of
DF . (
b,
c)
= dist (
b,
c) )
by METRIC_1:def 1;
hence
the
distance of
DF . (
a,
c)
<= ( the distance of DF . (a,b)) + ( the distance of DF . (b,c))
by A2, METRIC_1:4;
verum
end;
hence
f is_metric_of D
;
verum
end;
( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )
proof
assume A3:
f is_metric_of D
;
MetrStruct(# D,f #) is MetrSpace
for
a,
b,
c being
Element of
MetrStruct(#
D,
f #) holds
( (
dist (
a,
b)
= 0 implies
a = b ) & (
a = b implies
dist (
a,
b)
= 0 ) &
dist (
a,
b)
= dist (
b,
a) &
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c)) )
proof
let a,
b,
c be
Element of
MetrStruct(#
D,
f #);
( ( dist (a,b) = 0 implies a = b ) & ( a = b implies dist (a,b) = 0 ) & dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
A4:
the
distance of
MetrStruct(#
D,
f #)
. (
a,
b)
= dist (
a,
b)
by METRIC_1:def 1;
hence
(
dist (
a,
b)
= 0 iff
a = b )
by A3;
( dist (a,b) = dist (b,a) & dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
the
distance of
MetrStruct(#
D,
f #)
. (
b,
a)
= dist (
b,
a)
by METRIC_1:def 1;
hence
dist (
a,
b)
= dist (
b,
a)
by A3, A4;
dist (a,c) <= (dist (a,b)) + (dist (b,c))
( the
distance of
MetrStruct(#
D,
f #)
. (
a,
c)
= dist (
a,
c) & the
distance of
MetrStruct(#
D,
f #)
. (
b,
c)
= dist (
b,
c) )
by METRIC_1:def 1;
hence
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
by A3, A4;
verum
end;
hence
MetrStruct(#
D,
f #) is
MetrSpace
by METRIC_1:6;
verum
end;
hence
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
by A1; verum