let A be non empty set ; for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric (A,G) is_metric_of A
let G be Function of [:A,A:],REAL; ( G is_metric_of A implies bounded_metric (A,G) is_metric_of A )
assume A1:
G is_metric_of A
; bounded_metric (A,G) is_metric_of A
A2:
for a, b, c being Element of A holds (bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c))
proof
let a,
b,
c be
Element of
A;
(bounded_metric (A,G)) . (a,c) <= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c))
set a1 =
G . (
a,
b);
set a3 =
G . (
a,
c);
set a5 =
G . (
b,
c);
A3:
(
(bounded_metric (A,G)) . (
a,
b)
= (G . (a,b)) / (1 + (G . (a,b))) &
(bounded_metric (A,G)) . (
a,
c)
= (G . (a,c)) / (1 + (G . (a,c))) )
by Def1;
A4:
(bounded_metric (A,G)) . (
b,
c)
= (G . (b,c)) / (1 + (G . (b,c)))
by Def1;
A5:
G . (
a,
c)
>= 0
by A1, Th2;
A6:
(
0 <= G . (
a,
b) &
0 <= G . (
b,
c) )
by A1, Th2;
then A7:
0 <> (1 + (G . (a,b))) * (1 + (G . (b,c)))
by XCMPLX_1:6;
A8:
((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c)))) =
(((G . (a,b)) * (1 + (G . (b,c)))) + ((G . (b,c)) * (1 + (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c))))
by A6, XCMPLX_1:116
.=
((((G . (a,b)) * 1) + ((G . (a,b)) * (G . (b,c)))) + (((G . (b,c)) * 1) + ((G . (b,c)) * (G . (a,b))))) / ((1 + (G . (a,b))) * (1 + (G . (b,c))))
;
0 <= G . (
a,
c)
by A1, Th2;
then A9:
(((G . (a,b)) / (1 + (G . (a,b)))) + ((G . (b,c)) / (1 + (G . (b,c))))) - ((G . (a,c)) / (1 + (G . (a,c)))) = (((((G . (a,b)) + ((G . (a,b)) * (G . (b,c)))) + ((G . (b,c)) + ((G . (b,c)) * (G . (a,b))))) * (1 + (G . (a,c)))) - ((G . (a,c)) * ((1 + (G . (a,b))) * (1 + (G . (b,c)))))) / (((1 + (G . (a,b))) * (1 + (G . (b,c)))) * (1 + (G . (a,c))))
by A7, A8, XCMPLX_1:130;
A10:
(
G . (
a,
b)
>= 0 &
G . (
b,
c)
>= 0 )
by A1, Th2;
G . (
a,
c)
<= (G . (a,b)) + (G . (b,c))
by A1, PCOMPS_1:def 6;
then
((G . (a,b)) + (G . (b,c))) - (G . (a,c)) >= 0
by XREAL_1:48;
then
(((G . (b,c)) + (G . (a,b))) - (G . (a,c))) + (((G . (a,b)) * (G . (b,c))) + (((G . (b,c)) * (G . (a,b))) + (((G . (b,c)) * (G . (a,b))) * (G . (a,c))))) >= 0
by A10, A5;
hence
(bounded_metric (A,G)) . (
a,
c)
<= ((bounded_metric (A,G)) . (a,b)) + ((bounded_metric (A,G)) . (b,c))
by A3, A4, A9, A10, A5, XREAL_1:49;
verum
end;
A11:
for a, b being Element of A holds
( (bounded_metric (A,G)) . (a,b) = 0 iff a = b )
for a, b being Element of A holds (bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a)
proof
let a,
b be
Element of
A;
(bounded_metric (A,G)) . (a,b) = (bounded_metric (A,G)) . (b,a)
(G . (a,b)) / (1 + (G . (a,b))) =
(G . (b,a)) / (1 + (G . (a,b)))
by A1, PCOMPS_1:def 6
.=
(G . (b,a)) / (1 + (G . (b,a)))
by A1, PCOMPS_1:def 6
.=
(bounded_metric (A,G)) . (
b,
a)
by Def1
;
hence
(bounded_metric (A,G)) . (
a,
b)
= (bounded_metric (A,G)) . (
b,
a)
by Def1;
verum
end;
hence
bounded_metric (A,G) is_metric_of A
by A11, A2, PCOMPS_1:def 6; verum