Metamath Proof Explorer


Theorem comet

Description: The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015)

Ref Expression
Hypotheses comet.1 φD∞MetX
comet.2 φF:0+∞*
comet.3 φx0+∞Fx=0x=0
comet.4 φx0+∞y0+∞xyFxFy
comet.5 φx0+∞y0+∞Fx+𝑒yFx+𝑒Fy
Assertion comet φFD∞MetX

Proof

Step Hyp Ref Expression
1 comet.1 φD∞MetX
2 comet.2 φF:0+∞*
3 comet.3 φx0+∞Fx=0x=0
4 comet.4 φx0+∞y0+∞xyFxFy
5 comet.5 φx0+∞y0+∞Fx+𝑒yFx+𝑒Fy
6 1 elfvexd φXV
7 xmetf D∞MetXD:X×X*
8 1 7 syl φD:X×X*
9 8 ffnd φDFnX×X
10 xmetcl D∞MetXaXbXaDb*
11 xmetge0 D∞MetXaXbX0aDb
12 elxrge0 aDb0+∞aDb*0aDb
13 10 11 12 sylanbrc D∞MetXaXbXaDb0+∞
14 13 3expb D∞MetXaXbXaDb0+∞
15 1 14 sylan φaXbXaDb0+∞
16 15 ralrimivva φaXbXaDb0+∞
17 ffnov D:X×X0+∞DFnX×XaXbXaDb0+∞
18 9 16 17 sylanbrc φD:X×X0+∞
19 2 18 fcod φFD:X×X*
20 opelxpi aXbXabX×X
21 fvco3 D:X×X*abX×XFDab=FDab
22 8 20 21 syl2an φaXbXFDab=FDab
23 df-ov aFDb=FDab
24 df-ov aDb=Dab
25 24 fveq2i FaDb=FDab
26 22 23 25 3eqtr4g φaXbXaFDb=FaDb
27 26 eqeq1d φaXbXaFDb=0FaDb=0
28 fveq2 x=aDbFx=FaDb
29 28 eqeq1d x=aDbFx=0FaDb=0
30 eqeq1 x=aDbx=0aDb=0
31 29 30 bibi12d x=aDbFx=0x=0FaDb=0aDb=0
32 3 ralrimiva φx0+∞Fx=0x=0
33 32 adantr φaXbXx0+∞Fx=0x=0
34 31 33 15 rspcdva φaXbXFaDb=0aDb=0
35 xmeteq0 D∞MetXaXbXaDb=0a=b
36 35 3expb D∞MetXaXbXaDb=0a=b
37 1 36 sylan φaXbXaDb=0a=b
38 27 34 37 3bitrd φaXbXaFDb=0a=b
39 2 adantr φaXbXcXF:0+∞*
40 15 3adantr3 φaXbXcXaDb0+∞
41 39 40 ffvelrnd φaXbXcXFaDb*
42 18 adantr φaXbXcXD:X×X0+∞
43 simpr3 φaXbXcXcX
44 simpr1 φaXbXcXaX
45 42 43 44 fovrnd φaXbXcXcDa0+∞
46 simpr2 φaXbXcXbX
47 42 43 46 fovrnd φaXbXcXcDb0+∞
48 ge0xaddcl cDa0+∞cDb0+∞cDa+𝑒cDb0+∞
49 45 47 48 syl2anc φaXbXcXcDa+𝑒cDb0+∞
50 39 49 ffvelrnd φaXbXcXFcDa+𝑒cDb*
51 39 45 ffvelrnd φaXbXcXFcDa*
52 39 47 ffvelrnd φaXbXcXFcDb*
53 51 52 xaddcld φaXbXcXFcDa+𝑒FcDb*
54 3anrot cXaXbXaXbXcX
55 xmettri2 D∞MetXcXaXbXaDbcDa+𝑒cDb
56 54 55 sylan2br D∞MetXaXbXcXaDbcDa+𝑒cDb
57 1 56 sylan φaXbXcXaDbcDa+𝑒cDb
58 4 ralrimivva φx0+∞y0+∞xyFxFy
59 58 adantr φaXbXcXx0+∞y0+∞xyFxFy
60 breq1 x=aDbxyaDby
61 28 breq1d x=aDbFxFyFaDbFy
62 60 61 imbi12d x=aDbxyFxFyaDbyFaDbFy
63 breq2 y=cDa+𝑒cDbaDbyaDbcDa+𝑒cDb
64 fveq2 y=cDa+𝑒cDbFy=FcDa+𝑒cDb
65 64 breq2d y=cDa+𝑒cDbFaDbFyFaDbFcDa+𝑒cDb
66 63 65 imbi12d y=cDa+𝑒cDbaDbyFaDbFyaDbcDa+𝑒cDbFaDbFcDa+𝑒cDb
67 62 66 rspc2va aDb0+∞cDa+𝑒cDb0+∞x0+∞y0+∞xyFxFyaDbcDa+𝑒cDbFaDbFcDa+𝑒cDb
68 40 49 59 67 syl21anc φaXbXcXaDbcDa+𝑒cDbFaDbFcDa+𝑒cDb
69 57 68 mpd φaXbXcXFaDbFcDa+𝑒cDb
70 5 ralrimivva φx0+∞y0+∞Fx+𝑒yFx+𝑒Fy
71 70 adantr φaXbXcXx0+∞y0+∞Fx+𝑒yFx+𝑒Fy
72 fvoveq1 x=cDaFx+𝑒y=FcDa+𝑒y
73 fveq2 x=cDaFx=FcDa
74 73 oveq1d x=cDaFx+𝑒Fy=FcDa+𝑒Fy
75 72 74 breq12d x=cDaFx+𝑒yFx+𝑒FyFcDa+𝑒yFcDa+𝑒Fy
76 oveq2 y=cDbcDa+𝑒y=cDa+𝑒cDb
77 76 fveq2d y=cDbFcDa+𝑒y=FcDa+𝑒cDb
78 fveq2 y=cDbFy=FcDb
79 78 oveq2d y=cDbFcDa+𝑒Fy=FcDa+𝑒FcDb
80 77 79 breq12d y=cDbFcDa+𝑒yFcDa+𝑒FyFcDa+𝑒cDbFcDa+𝑒FcDb
81 75 80 rspc2va cDa0+∞cDb0+∞x0+∞y0+∞Fx+𝑒yFx+𝑒FyFcDa+𝑒cDbFcDa+𝑒FcDb
82 45 47 71 81 syl21anc φaXbXcXFcDa+𝑒cDbFcDa+𝑒FcDb
83 41 50 53 69 82 xrletrd φaXbXcXFaDbFcDa+𝑒FcDb
84 26 3adantr3 φaXbXcXaFDb=FaDb
85 8 adantr φaXbXcXD:X×X*
86 43 44 opelxpd φaXbXcXcaX×X
87 85 86 fvco3d φaXbXcXFDca=FDca
88 df-ov cFDa=FDca
89 df-ov cDa=Dca
90 89 fveq2i FcDa=FDca
91 87 88 90 3eqtr4g φaXbXcXcFDa=FcDa
92 43 46 opelxpd φaXbXcXcbX×X
93 85 92 fvco3d φaXbXcXFDcb=FDcb
94 df-ov cFDb=FDcb
95 df-ov cDb=Dcb
96 95 fveq2i FcDb=FDcb
97 93 94 96 3eqtr4g φaXbXcXcFDb=FcDb
98 91 97 oveq12d φaXbXcXcFDa+𝑒cFDb=FcDa+𝑒FcDb
99 83 84 98 3brtr4d φaXbXcXaFDbcFDa+𝑒cFDb
100 6 19 38 99 isxmetd φFD∞MetX