let A be non empty set ; :: thesis: 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 ; :: thesis: ( G is_metric_of A implies bounded_metric A,G is_metric_of A )
assume A1:
G is_metric_of A
; :: thesis: bounded_metric A,G is_metric_of A
A2:
for a, b being Element of A holds
( (bounded_metric A,G) . a,b = 0 iff a = b )
proof
let a,
b be
Element of
A;
:: thesis: ( (bounded_metric A,G) . a,b = 0 iff a = b )
A3:
(
(bounded_metric A,G) . a,
b = 0 implies
a = b )
proof
assume
(bounded_metric A,G) . a,
b = 0
;
:: thesis: a = b
then A4:
(G . a,b) / (1 + (G . a,b)) = 0
by Def4;
0 <= G . a,
b
by A1, Th2;
then
0 + 1
<= (G . a,b) + 1
by XREAL_1:8;
then
G . a,
b = 0
by A4, XCMPLX_1:50;
hence
a = b
by A1, PCOMPS_1:def 7;
:: thesis: verum
end;
(
a = b implies
(bounded_metric A,G) . a,
b = 0 )
hence
(
(bounded_metric A,G) . a,
b = 0 iff
a = b )
by A3;
:: thesis: verum
end;
A5:
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;
:: thesis: (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 7
.=
(G . b,a) / (1 + (G . b,a))
by A1, PCOMPS_1:def 7
.=
(bounded_metric A,G) . b,
a
by Def4
;
hence
(bounded_metric A,G) . a,
b = (bounded_metric A,G) . b,
a
by Def4;
:: thesis: verum
end;
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;
:: thesis: (bounded_metric A,G) . a,c <= ((bounded_metric A,G) . a,b) + ((bounded_metric A,G) . b,c)
A6:
(bounded_metric A,G) . a,
b = (G . a,b) / (1 + (G . a,b))
by Def4;
A7:
(bounded_metric A,G) . a,
c = (G . a,c) / (1 + (G . a,c))
by Def4;
A8:
(bounded_metric A,G) . b,
c = (G . b,c) / (1 + (G . b,c))
by Def4;
0 <= G . a,
b
by A1, Th2;
then A9:
0 + 1
<= (G . a,b) + 1
by XREAL_1:8;
0 <= G . b,
c
by A1, Th2;
then A10:
0 + 1
<= (G . b,c) + 1
by XREAL_1:8;
0 <= G . a,
c
by A1, Th2;
then A11:
0 + 1
<= (G . a,c) + 1
by XREAL_1:8;
set a1 =
G . a,
b;
set a3 =
G . a,
c;
set a5 =
G . b,
c;
A12:
0 <> (1 + (G . a,b)) * (1 + (G . b,c))
by A9, A10, XCMPLX_1:6;
((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 A9, A10, XCMPLX_1:117
.=
((((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)))
;
then A13:
(((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 A11, A12, XCMPLX_1:131;
G . a,
c <= (G . a,b) + (G . b,c)
by A1, PCOMPS_1:def 7;
then A14:
((G . a,b) + (G . b,c)) - (G . a,c) >= 0
by XREAL_1:50;
A15:
G . a,
b >= 0
by A1, Th2;
A16:
G . b,
c >= 0
by A1, Th2;
A17:
G . a,
c >= 0
by A1, Th2;
A18:
(G . a,b) * (G . b,c) >= 0
by A15, A16;
A19:
(G . b,c) * (G . a,b) >= 0
by A15, A16;
then
((G . b,c) * (G . a,b)) * (G . a,c) >= 0
by A17;
then
((G . b,c) * (G . a,b)) + (((G . b,c) * (G . a,b)) * (G . a,c)) >= 0 + 0
by A19;
then
((G . a,b) * (G . b,c)) + (((G . b,c) * (G . a,b)) + (((G . b,c) * (G . a,b)) * (G . a,c))) >= 0 + 0
by A18;
then A20:
(((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 A14;
A21:
0 + 1
<= (G . a,b) + 1
by A15, XREAL_1:8;
A22:
0 + 1
<= (G . a,c) + 1
by A17, XREAL_1:8;
0 + 1
<= (G . b,c) + 1
by A16, XREAL_1:8;
then
(1 + (G . a,b)) * (1 + (G . b,c)) > 0
by A21, XREAL_1:131;
then
((1 + (G . a,b)) * (1 + (G . b,c))) * (1 + (G . a,c)) > 0
by A22, XREAL_1:131;
then
(((G . a,b) / (1 + (G . a,b))) + ((G . b,c) / (1 + (G . b,c)))) - ((G . a,c) / (1 + (G . a,c))) >= 0
by A13, A20;
hence
(bounded_metric A,G) . a,
c <= ((bounded_metric A,G) . a,b) + ((bounded_metric A,G) . b,c)
by A6, A7, A8, XREAL_1:51;
:: thesis: verum
end;
hence
bounded_metric A,G is_metric_of A
by A2, A5, PCOMPS_1:def 7; :: thesis: verum