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: ( MetrStruct(# D,f #) is MetrSpace implies f is_metric_of D )

proof

assume A2: 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) )
A3: 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 A2, 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 A2, A3, 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)
( 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 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 A2, A3, METRIC_1:4; :: thesis: verum

end;

hence f is_metric_of D by Def7; :: thesis: verum

end;

( f is_metric_of D implies MetrStruct(# D,f #) is MetrSpace )

proof

assume A4: 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) )
A5: 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 A4, 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 A4, A5, Def7; :: thesis: 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 A4, A5, Def7; :: thesis: verum

end;

hence MetrStruct(# D,f #) is MetrSpace by METRIC_1:6; :: thesis: verum

end;

hence ( f is_metric_of D iff MetrStruct(# D,f #) is MetrSpace ) by A1; :: thesis: verum