let D be set ; :: thesis: 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 ; :: thesis: ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
set DF = MetrStruct(# D,f #);
A1:
( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )
proof
assume A2:
f is_metric_of D
;
:: thesis: 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 #);
:: thesis: ( ( 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) )
A3:
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 A2, Def7;
:: thesis: ( 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 A2, A3, Def7;
:: thesis: dist a,c <= (dist a,b) + (dist b,c)
A4:
the
distance of
MetrStruct(#
D,
f #)
. a,
c = dist a,
c
by METRIC_1:def 1;
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 A2, A3, A4, Def7;
:: thesis: verum
end;
hence
MetrStruct(#
D,
f #) is
MetrSpace
by METRIC_1:6;
:: thesis: verum
end;
( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )
proof
assume A5:
MetrStruct(#
D,
f #) is
MetrSpace
;
:: thesis: f is_metric_of D
for
a,
b,
c being
Element of
MetrStruct(#
D,
f #) holds
( ( the
distance of
MetrStruct(#
D,
f #)
. a,
b = 0 implies
a = b ) & (
a = b implies the
distance of
MetrStruct(#
D,
f #)
. a,
b = 0 ) & the
distance of
MetrStruct(#
D,
f #)
. a,
b = the
distance of
MetrStruct(#
D,
f #)
. b,
a & the
distance of
MetrStruct(#
D,
f #)
. a,
c <= (the distance of MetrStruct(# D,f #) . a,b) + (the distance of MetrStruct(# D,f #) . b,c) )
proof
let a,
b,
c be
Element of
MetrStruct(#
D,
f #);
:: thesis: ( ( the distance of MetrStruct(# D,f #) . a,b = 0 implies a = b ) & ( a = b implies the distance of MetrStruct(# D,f #) . a,b = 0 ) & the distance of MetrStruct(# D,f #) . a,b = the distance of MetrStruct(# D,f #) . b,a & the distance of MetrStruct(# D,f #) . a,c <= (the distance of MetrStruct(# D,f #) . a,b) + (the distance of MetrStruct(# D,f #) . b,c) )
A6:
the
distance of
MetrStruct(#
D,
f #)
. a,
b = dist a,
b
by METRIC_1:def 1;
hence
( the
distance of
MetrStruct(#
D,
f #)
. a,
b = 0 iff
a = b )
by A5, METRIC_1:1, METRIC_1:2;
:: thesis: ( the distance of MetrStruct(# D,f #) . a,b = the distance of MetrStruct(# D,f #) . b,a & the distance of MetrStruct(# D,f #) . a,c <= (the distance of MetrStruct(# D,f #) . a,b) + (the distance of MetrStruct(# D,f #) . b,c) )
the
distance of
MetrStruct(#
D,
f #)
. b,
a = dist b,
a
by METRIC_1:def 1;
hence
the
distance of
MetrStruct(#
D,
f #)
. a,
b = the
distance of
MetrStruct(#
D,
f #)
. b,
a
by A5, A6, METRIC_1:3;
:: thesis: the distance of MetrStruct(# D,f #) . a,c <= (the distance of MetrStruct(# D,f #) . a,b) + (the distance of MetrStruct(# D,f #) . b,c)
A7:
the
distance of
MetrStruct(#
D,
f #)
. a,
c = dist a,
c
by METRIC_1:def 1;
the
distance of
MetrStruct(#
D,
f #)
. b,
c = dist b,
c
by METRIC_1:def 1;
hence
the
distance of
MetrStruct(#
D,
f #)
. a,
c <= (the distance of MetrStruct(# D,f #) . a,b) + (the distance of MetrStruct(# D,f #) . b,c)
by A5, A6, A7, METRIC_1:4;
:: thesis: verum
end;
hence
f is_metric_of D
by Def7;
:: thesis: verum
end;
hence
( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace )
by A1; :: thesis: verum