Metamath Proof Explorer


Theorem prdsxmetlem

Description: The product metric is an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses prdsdsf.y ⊒Y=S⨉𝑠x∈I⟼R
prdsdsf.b ⊒B=BaseY
prdsdsf.v ⊒V=BaseR
prdsdsf.e ⊒E=dist⁑Rβ†ΎVΓ—V
prdsdsf.d ⊒D=dist⁑Y
prdsdsf.s βŠ’Ο†β†’S∈W
prdsdsf.i βŠ’Ο†β†’I∈X
prdsdsf.r βŠ’Ο†βˆ§x∈Iβ†’R∈Z
prdsdsf.m βŠ’Ο†βˆ§x∈Iβ†’E∈∞Met⁑V
Assertion prdsxmetlem βŠ’Ο†β†’D∈∞Met⁑B

Proof

Step Hyp Ref Expression
1 prdsdsf.y ⊒Y=S⨉𝑠x∈I⟼R
2 prdsdsf.b ⊒B=BaseY
3 prdsdsf.v ⊒V=BaseR
4 prdsdsf.e ⊒E=dist⁑Rβ†ΎVΓ—V
5 prdsdsf.d ⊒D=dist⁑Y
6 prdsdsf.s βŠ’Ο†β†’S∈W
7 prdsdsf.i βŠ’Ο†β†’I∈X
8 prdsdsf.r βŠ’Ο†βˆ§x∈Iβ†’R∈Z
9 prdsdsf.m βŠ’Ο†βˆ§x∈Iβ†’E∈∞Met⁑V
10 2 fvexi ⊒B∈V
11 10 a1i βŠ’Ο†β†’B∈V
12 1 2 3 4 5 6 7 8 9 prdsdsf βŠ’Ο†β†’D:BΓ—B⟢0+∞
13 iccssxr ⊒0+βˆžβŠ†β„*
14 fss ⊒D:BΓ—B⟢0+∞∧0+βˆžβŠ†β„*β†’D:BΓ—BβŸΆβ„*
15 12 13 14 sylancl βŠ’Ο†β†’D:BΓ—BβŸΆβ„*
16 12 fovrnda βŠ’Ο†βˆ§f∈B∧g∈Bβ†’fDg∈0+∞
17 elxrge0 ⊒fDg∈0+βˆžβ†”fDgβˆˆβ„*∧0≀fDg
18 17 simprbi ⊒fDg∈0+βˆžβ†’0≀fDg
19 16 18 syl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0≀fDg
20 6 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’S∈W
21 7 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’I∈X
22 8 ralrimiva βŠ’Ο†β†’βˆ€x∈IR∈Z
23 22 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈IR∈Z
24 simprl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’f∈B
25 simprr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’g∈B
26 1 2 20 21 23 24 25 3 4 5 prdsdsval3 βŠ’Ο†βˆ§f∈B∧g∈Bβ†’fDg=supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<
27 26 breq1d βŠ’Ο†βˆ§f∈B∧g∈Bβ†’fDg≀0↔supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀0
28 9 adantlr βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’E∈∞Met⁑V
29 1 2 20 21 23 3 24 prdsbascl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈If⁑x∈V
30 29 r19.21bi βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑x∈V
31 1 2 20 21 23 3 25 prdsbascl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈Ig⁑x∈V
32 31 r19.21bi βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’g⁑x∈V
33 xmetcl ⊒E∈∞Met⁑V∧f⁑x∈V∧g⁑x∈Vβ†’f⁑xEg⁑xβˆˆβ„*
34 28 30 32 33 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑xEg⁑xβˆˆβ„*
35 34 fmpttd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’x∈I⟼f⁑xEg⁑x:IβŸΆβ„*
36 35 frnd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’ran⁑x∈I⟼f⁑xEg⁑xβŠ†β„*
37 0xr ⊒0βˆˆβ„*
38 37 a1i βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0βˆˆβ„*
39 38 snssd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’0βŠ†β„*
40 36 39 unssd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0βŠ†β„*
41 supxrleub ⊒ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0βŠ†β„*∧0βˆˆβ„*β†’supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀0β†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0
42 40 37 41 sylancl βŠ’Ο†βˆ§f∈B∧g∈Bβ†’supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀0β†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0
43 0le0 ⊒0≀0
44 c0ex ⊒0∈V
45 breq1 ⊒z=0β†’z≀0↔0≀0
46 44 45 ralsn βŠ’βˆ€z∈0z≀0↔0≀0
47 43 46 mpbir βŠ’βˆ€z∈0z≀0
48 ralunb βŠ’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0β†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀0βˆ§βˆ€z∈0z≀0
49 47 48 mpbiran2 βŠ’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0β†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀0
50 ovex ⊒f⁑xEg⁑x∈V
51 50 rgenw βŠ’βˆ€x∈If⁑xEg⁑x∈V
52 eqid ⊒x∈I⟼f⁑xEg⁑x=x∈I⟼f⁑xEg⁑x
53 breq1 ⊒z=f⁑xEg⁑xβ†’z≀0↔f⁑xEg⁑x≀0
54 52 53 ralrnmptw βŠ’βˆ€x∈If⁑xEg⁑x∈Vβ†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀0β†”βˆ€x∈If⁑xEg⁑x≀0
55 51 54 ax-mp βŠ’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀0β†”βˆ€x∈If⁑xEg⁑x≀0
56 49 55 bitri βŠ’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0β†”βˆ€x∈If⁑xEg⁑x≀0
57 xmetge0 ⊒E∈∞Met⁑V∧f⁑x∈V∧g⁑x∈Vβ†’0≀f⁑xEg⁑x
58 28 30 32 57 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’0≀f⁑xEg⁑x
59 58 biantrud βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑xEg⁑x≀0↔f⁑xEg⁑x≀0∧0≀f⁑xEg⁑x
60 xrletri3 ⊒f⁑xEg⁑xβˆˆβ„*∧0βˆˆβ„*β†’f⁑xEg⁑x=0↔f⁑xEg⁑x≀0∧0≀f⁑xEg⁑x
61 34 37 60 sylancl βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑xEg⁑x=0↔f⁑xEg⁑x≀0∧0≀f⁑xEg⁑x
62 xmeteq0 ⊒E∈∞Met⁑V∧f⁑x∈V∧g⁑x∈Vβ†’f⁑xEg⁑x=0↔f⁑x=g⁑x
63 28 30 32 62 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑xEg⁑x=0↔f⁑x=g⁑x
64 59 61 63 3bitr2d βŠ’Ο†βˆ§f∈B∧g∈B∧x∈Iβ†’f⁑xEg⁑x≀0↔f⁑x=g⁑x
65 64 ralbidva βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈If⁑xEg⁑x≀0β†”βˆ€x∈If⁑x=g⁑x
66 eqid ⊒x∈I⟼R=x∈I⟼R
67 66 fnmpt βŠ’βˆ€x∈IR∈Zβ†’x∈I⟼RFnI
68 22 67 syl βŠ’Ο†β†’x∈I⟼RFnI
69 68 adantr βŠ’Ο†βˆ§f∈B∧g∈Bβ†’x∈I⟼RFnI
70 1 2 20 21 69 24 prdsbasfn βŠ’Ο†βˆ§f∈B∧g∈Bβ†’fFnI
71 1 2 20 21 69 25 prdsbasfn βŠ’Ο†βˆ§f∈B∧g∈Bβ†’gFnI
72 eqfnfv ⊒fFnI∧gFnIβ†’f=gβ†”βˆ€x∈If⁑x=g⁑x
73 70 71 72 syl2anc βŠ’Ο†βˆ§f∈B∧g∈Bβ†’f=gβ†”βˆ€x∈If⁑x=g⁑x
74 65 73 bitr4d βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€x∈If⁑xEg⁑x≀0↔f=g
75 56 74 syl5bb βŠ’Ο†βˆ§f∈B∧g∈Bβ†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀0↔f=g
76 27 42 75 3bitrd βŠ’Ο†βˆ§f∈B∧g∈Bβ†’fDg≀0↔f=g
77 26 3adantr3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈Bβ†’fDg=supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<
78 77 3adant3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’fDg=supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<
79 9 3ad2antl1 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’E∈∞Met⁑V
80 29 3adantr3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈Bβ†’βˆ€x∈If⁑x∈V
81 80 3adant3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈If⁑x∈V
82 81 r19.21bi βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑x∈V
83 31 3adantr3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈Bβ†’βˆ€x∈Ig⁑x∈V
84 83 3adant3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈Ig⁑x∈V
85 84 r19.21bi βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’g⁑x∈V
86 79 82 85 33 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑xEg⁑xβˆˆβ„*
87 6 3ad2ant1 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’S∈W
88 7 3ad2ant1 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’I∈X
89 22 3ad2ant1 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈IR∈Z
90 simp23 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’h∈B
91 1 2 87 88 89 3 90 prdsbascl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈Ih⁑x∈V
92 91 r19.21bi βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑x∈V
93 xmetcl ⊒E∈∞Met⁑V∧h⁑x∈V∧f⁑x∈Vβ†’h⁑xEf⁑xβˆˆβ„*
94 79 92 82 93 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑xβˆˆβ„*
95 simp3l βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDfβˆˆβ„
96 95 adantr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’hDfβˆˆβ„
97 xmetge0 ⊒E∈∞Met⁑V∧h⁑x∈V∧f⁑x∈Vβ†’0≀h⁑xEf⁑x
98 79 92 82 97 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’0≀h⁑xEf⁑x
99 94 fmpttd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’x∈I⟼h⁑xEf⁑x:IβŸΆβ„*
100 99 frnd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’ran⁑x∈I⟼h⁑xEf⁑xβŠ†β„*
101 37 a1i βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’0βˆˆβ„*
102 101 snssd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’0βŠ†β„*
103 100 102 unssd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’ran⁑x∈I⟼h⁑xEf⁑xβˆͺ0βŠ†β„*
104 ssun1 ⊒ran⁑x∈I⟼h⁑xEf⁑xβŠ†ran⁑x∈I⟼h⁑xEf⁑xβˆͺ0
105 ovex ⊒h⁑xEf⁑x∈V
106 105 elabrex ⊒x∈Iβ†’h⁑xEf⁑x∈z|βˆƒx∈Iz=h⁑xEf⁑x
107 106 adantl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x∈z|βˆƒx∈Iz=h⁑xEf⁑x
108 eqid ⊒x∈I⟼h⁑xEf⁑x=x∈I⟼h⁑xEf⁑x
109 108 rnmpt ⊒ran⁑x∈I⟼h⁑xEf⁑x=z|βˆƒx∈Iz=h⁑xEf⁑x
110 107 109 eleqtrrdi βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x∈ran⁑x∈I⟼h⁑xEf⁑x
111 104 110 sselid βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x∈ran⁑x∈I⟼h⁑xEf⁑xβˆͺ0
112 supxrub ⊒ran⁑x∈I⟼h⁑xEf⁑xβˆͺ0βŠ†β„*∧h⁑xEf⁑x∈ran⁑x∈I⟼h⁑xEf⁑xβˆͺ0β†’h⁑xEf⁑x≀supran⁑x∈I⟼h⁑xEf⁑xβˆͺ0ℝ*<
113 103 111 112 syl2an2r βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x≀supran⁑x∈I⟼h⁑xEf⁑xβˆͺ0ℝ*<
114 simp21 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’f∈B
115 1 2 87 88 89 90 114 3 4 5 prdsdsval3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDf=supran⁑x∈I⟼h⁑xEf⁑xβˆͺ0ℝ*<
116 115 adantr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’hDf=supran⁑x∈I⟼h⁑xEf⁑xβˆͺ0ℝ*<
117 113 116 breqtrrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x≀hDf
118 xrrege0 ⊒h⁑xEf⁑xβˆˆβ„*∧hDfβˆˆβ„βˆ§0≀h⁑xEf⁑x∧h⁑xEf⁑x≀hDfβ†’h⁑xEf⁑xβˆˆβ„
119 94 96 98 117 118 syl22anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑xβˆˆβ„
120 xmetcl ⊒E∈∞Met⁑V∧h⁑x∈V∧g⁑x∈Vβ†’h⁑xEg⁑xβˆˆβ„*
121 79 92 85 120 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑xβˆˆβ„*
122 simp3r βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDgβˆˆβ„
123 122 adantr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’hDgβˆˆβ„
124 xmetge0 ⊒E∈∞Met⁑V∧h⁑x∈V∧g⁑x∈Vβ†’0≀h⁑xEg⁑x
125 79 92 85 124 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’0≀h⁑xEg⁑x
126 121 fmpttd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’x∈I⟼h⁑xEg⁑x:IβŸΆβ„*
127 126 frnd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’ran⁑x∈I⟼h⁑xEg⁑xβŠ†β„*
128 127 102 unssd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’ran⁑x∈I⟼h⁑xEg⁑xβˆͺ0βŠ†β„*
129 ssun1 ⊒ran⁑x∈I⟼h⁑xEg⁑xβŠ†ran⁑x∈I⟼h⁑xEg⁑xβˆͺ0
130 ovex ⊒h⁑xEg⁑x∈V
131 130 elabrex ⊒x∈Iβ†’h⁑xEg⁑x∈z|βˆƒx∈Iz=h⁑xEg⁑x
132 131 adantl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑x∈z|βˆƒx∈Iz=h⁑xEg⁑x
133 eqid ⊒x∈I⟼h⁑xEg⁑x=x∈I⟼h⁑xEg⁑x
134 133 rnmpt ⊒ran⁑x∈I⟼h⁑xEg⁑x=z|βˆƒx∈Iz=h⁑xEg⁑x
135 132 134 eleqtrrdi βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑x∈ran⁑x∈I⟼h⁑xEg⁑x
136 129 135 sselid βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑x∈ran⁑x∈I⟼h⁑xEg⁑xβˆͺ0
137 supxrub ⊒ran⁑x∈I⟼h⁑xEg⁑xβˆͺ0βŠ†β„*∧h⁑xEg⁑x∈ran⁑x∈I⟼h⁑xEg⁑xβˆͺ0β†’h⁑xEg⁑x≀supran⁑x∈I⟼h⁑xEg⁑xβˆͺ0ℝ*<
138 128 136 137 syl2an2r βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑x≀supran⁑x∈I⟼h⁑xEg⁑xβˆͺ0ℝ*<
139 simp22 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’g∈B
140 1 2 87 88 89 90 139 3 4 5 prdsdsval3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDg=supran⁑x∈I⟼h⁑xEg⁑xβˆͺ0ℝ*<
141 140 adantr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’hDg=supran⁑x∈I⟼h⁑xEg⁑xβˆͺ0ℝ*<
142 138 141 breqtrrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑x≀hDg
143 xrrege0 ⊒h⁑xEg⁑xβˆˆβ„*∧hDgβˆˆβ„βˆ§0≀h⁑xEg⁑x∧h⁑xEg⁑x≀hDgβ†’h⁑xEg⁑xβˆˆβ„
144 121 123 125 142 143 syl22anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEg⁑xβˆˆβ„
145 119 144 readdcld βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x+h⁑xEg⁑xβˆˆβ„
146 79 82 85 57 syl3anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’0≀f⁑xEg⁑x
147 xmettri2 ⊒E∈∞Met⁑V∧h⁑x∈V∧f⁑x∈V∧g⁑x∈Vβ†’f⁑xEg⁑x≀h⁑xEf⁑x+𝑒h⁑xEg⁑x
148 79 92 82 85 147 syl13anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑xEg⁑x≀h⁑xEf⁑x+𝑒h⁑xEg⁑x
149 119 144 rexaddd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x+𝑒h⁑xEg⁑x=h⁑xEf⁑x+h⁑xEg⁑x
150 148 149 breqtrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑xEg⁑x≀h⁑xEf⁑x+h⁑xEg⁑x
151 xrrege0 ⊒f⁑xEg⁑xβˆˆβ„*∧h⁑xEf⁑x+h⁑xEg⁑xβˆˆβ„βˆ§0≀f⁑xEg⁑x∧f⁑xEg⁑x≀h⁑xEf⁑x+h⁑xEg⁑xβ†’f⁑xEg⁑xβˆˆβ„
152 86 145 146 150 151 syl22anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑xEg⁑xβˆˆβ„
153 readdcl ⊒hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDf+hDgβˆˆβ„
154 153 3ad2ant3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDf+hDgβˆˆβ„
155 154 adantr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’hDf+hDgβˆˆβ„
156 119 144 96 123 117 142 le2addd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’h⁑xEf⁑x+h⁑xEg⁑x≀hDf+hDg
157 152 145 155 150 156 letrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„βˆ§x∈Iβ†’f⁑xEg⁑x≀hDf+hDg
158 157 ralrimiva βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈If⁑xEg⁑x≀hDf+hDg
159 86 ralrimiva βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€x∈If⁑xEg⁑xβˆˆβ„*
160 breq1 ⊒z=f⁑xEg⁑xβ†’z≀hDf+hDg↔f⁑xEg⁑x≀hDf+hDg
161 52 160 ralrnmptw βŠ’βˆ€x∈If⁑xEg⁑xβˆˆβ„*β†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀hDf+hDgβ†”βˆ€x∈If⁑xEg⁑x≀hDf+hDg
162 159 161 syl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀hDf+hDgβ†”βˆ€x∈If⁑xEg⁑x≀hDf+hDg
163 158 162 mpbird βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀hDf+hDg
164 12 3ad2ant1 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’D:BΓ—B⟢0+∞
165 164 90 114 fovrnd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDf∈0+∞
166 elxrge0 ⊒hDf∈0+βˆžβ†”hDfβˆˆβ„*∧0≀hDf
167 166 simprbi ⊒hDf∈0+βˆžβ†’0≀hDf
168 165 167 syl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’0≀hDf
169 164 90 139 fovrnd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDg∈0+∞
170 elxrge0 ⊒hDg∈0+βˆžβ†”hDgβˆˆβ„*∧0≀hDg
171 170 simprbi ⊒hDg∈0+βˆžβ†’0≀hDg
172 169 171 syl βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’0≀hDg
173 95 122 168 172 addge0d βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’0≀hDf+hDg
174 breq1 ⊒z=0β†’z≀hDf+hDg↔0≀hDf+hDg
175 44 174 ralsn βŠ’βˆ€z∈0z≀hDf+hDg↔0≀hDf+hDg
176 173 175 sylibr βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€z∈0z≀hDf+hDg
177 ralunb βŠ’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀hDf+hDgβ†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xz≀hDf+hDgβˆ§βˆ€z∈0z≀hDf+hDg
178 163 176 177 sylanbrc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀hDf+hDg
179 40 3adantr3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈Bβ†’ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0βŠ†β„*
180 179 3adant3 βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0βŠ†β„*
181 154 rexrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’hDf+hDgβˆˆβ„*
182 supxrleub ⊒ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0βŠ†β„*∧hDf+hDgβˆˆβ„*β†’supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀hDf+hDgβ†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀hDf+hDg
183 180 181 182 syl2anc βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀hDf+hDgβ†”βˆ€z∈ran⁑x∈I⟼f⁑xEg⁑xβˆͺ0z≀hDf+hDg
184 178 183 mpbird βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’supran⁑x∈I⟼f⁑xEg⁑xβˆͺ0ℝ*<≀hDf+hDg
185 78 184 eqbrtrd βŠ’Ο†βˆ§f∈B∧g∈B∧h∈B∧hDfβˆˆβ„βˆ§hDgβˆˆβ„β†’fDg≀hDf+hDg
186 11 15 19 76 185 isxmet2d βŠ’Ο†β†’D∈∞Met⁑B