Metamath Proof Explorer


Theorem hoidmv1le

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal to the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is one of the two base cases of the induction of Lemma 115B of Fremlin1 p. 29 (the other base case is the 0-dimensional case). This proof of the 1-dimensional case is given in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1le.l L=xFinax,bxifx=0kxvolakbk
hoidmv1le.z φZV
hoidmv1le.x X=Z
hoidmv1le.a φA:X
hoidmv1le.b φB:X
hoidmv1le.c φC:X
hoidmv1le.d φD:X
hoidmv1le.s φkXAkBkjkXCjkDjk
Assertion hoidmv1le φALXBsum^jCjLXDj

Proof

Step Hyp Ref Expression
1 hoidmv1le.l L=xFinax,bxifx=0kxvolakbk
2 hoidmv1le.z φZV
3 hoidmv1le.x X=Z
4 hoidmv1le.a φA:X
5 hoidmv1le.b φB:X
6 hoidmv1le.c φC:X
7 hoidmv1le.d φD:X
8 hoidmv1le.s φkXAkBkjkXCjkDjk
9 snidg ZVZZ
10 2 9 syl φZZ
11 10 3 eleqtrrdi φZX
12 5 11 ffvelrnd φBZ
13 4 11 ffvelrnd φAZ
14 12 13 resubcld φBZAZ
15 14 rexrd φBZAZ*
16 pnfxr +∞*
17 16 a1i φ+∞*
18 14 ltpnfd φBZAZ<+∞
19 15 17 18 xrltled φBZAZ+∞
20 19 ad2antrr φAZ<BZsum^jvolCjZDjZ=+∞BZAZ+∞
21 id sum^jvolCjZDjZ=+∞sum^jvolCjZDjZ=+∞
22 21 eqcomd sum^jvolCjZDjZ=+∞+∞=sum^jvolCjZDjZ
23 22 adantl φAZ<BZsum^jvolCjZDjZ=+∞+∞=sum^jvolCjZDjZ
24 20 23 breqtrd φAZ<BZsum^jvolCjZDjZ=+∞BZAZsum^jvolCjZDjZ
25 simpl φAZ<BZ¬sum^jvolCjZDjZ=+∞φAZ<BZ
26 simpr φAZ<BZ¬sum^jvolCjZDjZ=+∞¬sum^jvolCjZDjZ=+∞
27 nnex V
28 27 a1i φAZ<BZ¬sum^jvolCjZDjZ=+∞V
29 3 a1i φX=Z
30 snfi ZFin
31 30 a1i φZFin
32 29 31 eqeltrd φXFin
33 32 adantr φjXFin
34 11 ne0d φX
35 34 adantr φjX
36 6 ffvelrnda φjCjX
37 elmapi CjXCj:X
38 36 37 syl φjCj:X
39 7 ffvelrnda φjDjX
40 elmapi DjXDj:X
41 39 40 syl φjDj:X
42 1 33 35 38 41 hoidmvn0val φjCjLXDj=kXvolCjkDjk
43 3 prodeq1i kXvolCjkDjk=kZvolCjkDjk
44 43 a1i φjkXvolCjkDjk=kZvolCjkDjk
45 2 adantr φjZV
46 11 adantr φjZX
47 38 46 ffvelrnd φjCjZ
48 41 46 ffvelrnd φjDjZ
49 volicore CjZDjZvolCjZDjZ
50 47 48 49 syl2anc φjvolCjZDjZ
51 50 recnd φjvolCjZDjZ
52 fveq2 k=ZCjk=CjZ
53 fveq2 k=ZDjk=DjZ
54 52 53 oveq12d k=ZCjkDjk=CjZDjZ
55 54 fveq2d k=ZvolCjkDjk=volCjZDjZ
56 55 prodsn ZVvolCjZDjZkZvolCjkDjk=volCjZDjZ
57 45 51 56 syl2anc φjkZvolCjkDjk=volCjZDjZ
58 42 44 57 3eqtrd φjCjLXDj=volCjZDjZ
59 58 mpteq2dva φjCjLXDj=jvolCjZDjZ
60 fveq2 k=lak=al
61 fveq2 k=lbk=bl
62 60 61 oveq12d k=lakbk=albl
63 62 fveq2d k=lvolakbk=volalbl
64 63 cbvprodv kxvolakbk=lxvolalbl
65 ifeq2 kxvolakbk=lxvolalblifx=0kxvolakbk=ifx=0lxvolalbl
66 64 65 ax-mp ifx=0kxvolakbk=ifx=0lxvolalbl
67 66 a1i axbxifx=0kxvolakbk=ifx=0lxvolalbl
68 67 mpoeq3ia ax,bxifx=0kxvolakbk=ax,bxifx=0lxvolalbl
69 68 mpteq2i xFinax,bxifx=0kxvolakbk=xFinax,bxifx=0lxvolalbl
70 1 69 eqtri L=xFinax,bxifx=0lxvolalbl
71 70 33 38 41 hoidmvcl φjCjLXDj0+∞
72 eqid jCjLXDj=jCjLXDj
73 71 72 fmptd φjCjLXDj:0+∞
74 icossicc 0+∞0+∞
75 74 a1i φ0+∞0+∞
76 73 75 fssd φjCjLXDj:0+∞
77 59 76 feq1dd φjvolCjZDjZ:0+∞
78 77 ad2antrr φAZ<BZ¬sum^jvolCjZDjZ=+∞jvolCjZDjZ:0+∞
79 28 78 sge0repnf φAZ<BZ¬sum^jvolCjZDjZ=+∞sum^jvolCjZDjZ¬sum^jvolCjZDjZ=+∞
80 26 79 mpbird φAZ<BZ¬sum^jvolCjZDjZ=+∞sum^jvolCjZDjZ
81 13 ad2antrr φAZ<BZsum^jvolCjZDjZAZ
82 12 ad2antrr φAZ<BZsum^jvolCjZDjZBZ
83 simplr φAZ<BZsum^jvolCjZDjZAZ<BZ
84 eqid jCjZ=jCjZ
85 47 84 fmptd φjCjZ:
86 85 ad2antrr φAZ<BZsum^jvolCjZDjZjCjZ:
87 eqid jDjZ=jDjZ
88 48 87 fmptd φjDjZ:
89 88 ad2antrr φAZ<BZsum^jvolCjZDjZjDjZ:
90 3 eleq2i kXkZ
91 90 biimpi kXkZ
92 elsni kZk=Z
93 91 92 syl kXk=Z
94 93 54 syl kXCjkDjk=CjZDjZ
95 94 rgen kXCjkDjk=CjZDjZ
96 ixpeq2 kXCjkDjk=CjZDjZkXCjkDjk=kXCjZDjZ
97 95 96 ax-mp kXCjkDjk=kXCjZDjZ
98 97 a1i jkXCjkDjk=kXCjZDjZ
99 98 iuneq2i jkXCjkDjk=jkXCjZDjZ
100 99 a1i φjkXCjkDjk=jkXCjZDjZ
101 8 100 sseqtrd φkXAkBkjkXCjZDjZ
102 101 adantr φxAZBZkXAkBkjkXCjZDjZ
103 id xAZBZxAZBZ
104 eqidd xAZBZZx=Zx
105 opeq2 y=xZy=Zx
106 105 sneqd y=xZy=Zx
107 106 rspceeqv xAZBZZx=ZxyAZBZZx=Zy
108 103 104 107 syl2anc xAZBZyAZBZZx=Zy
109 108 adantl φxAZBZyAZBZZx=Zy
110 elixpsn ZVZxkZAZBZyAZBZZx=Zy
111 2 110 syl φZxkZAZBZyAZBZZx=Zy
112 111 adantr φxAZBZZxkZAZBZyAZBZZx=Zy
113 109 112 mpbird φxAZBZZxkZAZBZ
114 3 eqcomi Z=X
115 ixpeq1 Z=XkZAZBZ=kXAZBZ
116 114 115 ax-mp kZAZBZ=kXAZBZ
117 fveq2 k=ZAk=AZ
118 93 117 syl kXAk=AZ
119 fveq2 k=ZBk=BZ
120 93 119 syl kXBk=BZ
121 118 120 oveq12d kXAkBk=AZBZ
122 121 eqcomd kXAZBZ=AkBk
123 122 rgen kXAZBZ=AkBk
124 ixpeq2 kXAZBZ=AkBkkXAZBZ=kXAkBk
125 123 124 ax-mp kXAZBZ=kXAkBk
126 116 125 eqtri kZAZBZ=kXAkBk
127 126 a1i φkZAZBZ=kXAkBk
128 127 adantr φxAZBZkZAZBZ=kXAkBk
129 113 128 eleqtrd φxAZBZZxkXAkBk
130 102 129 sseldd φxAZBZZxjkXCjZDjZ
131 eliun ZxjkXCjZDjZjZxkXCjZDjZ
132 130 131 sylib φxAZBZjZxkXCjZDjZ
133 ixpeq1 X=ZkXCjZDjZ=kZCjZDjZ
134 3 133 ax-mp kXCjZDjZ=kZCjZDjZ
135 134 eleq2i ZxkXCjZDjZZxkZCjZDjZ
136 135 biimpi ZxkXCjZDjZZxkZCjZDjZ
137 136 adantl φZxkXCjZDjZZxkZCjZDjZ
138 elixpsn ZVZxkZCjZDjZyCjZDjZZx=Zy
139 2 138 syl φZxkZCjZDjZyCjZDjZZx=Zy
140 139 adantr φZxkXCjZDjZZxkZCjZDjZyCjZDjZZx=Zy
141 137 140 mpbid φZxkXCjZDjZyCjZDjZZx=Zy
142 opex ZxV
143 142 sneqr Zx=ZyZx=Zy
144 143 adantl φZx=ZyZx=Zy
145 vex xV
146 145 a1i φxV
147 opthg ZVxVZx=ZyZ=Zx=y
148 2 146 147 syl2anc φZx=ZyZ=Zx=y
149 148 adantr φZx=ZyZx=ZyZ=Zx=y
150 144 149 mpbid φZx=ZyZ=Zx=y
151 150 simprd φZx=Zyx=y
152 151 3adant2 φyCjZDjZZx=Zyx=y
153 simp2 φyCjZDjZZx=ZyyCjZDjZ
154 152 153 eqeltrd φyCjZDjZZx=ZyxCjZDjZ
155 154 3exp φyCjZDjZZx=ZyxCjZDjZ
156 155 adantr φZxkXCjZDjZyCjZDjZZx=ZyxCjZDjZ
157 156 rexlimdv φZxkXCjZDjZyCjZDjZZx=ZyxCjZDjZ
158 141 157 mpd φZxkXCjZDjZxCjZDjZ
159 158 ex φZxkXCjZDjZxCjZDjZ
160 159 ad2antrr φxAZBZjZxkXCjZDjZxCjZDjZ
161 160 reximdva φxAZBZjZxkXCjZDjZjxCjZDjZ
162 132 161 mpd φxAZBZjxCjZDjZ
163 eliun xjCjZDjZjxCjZDjZ
164 162 163 sylibr φxAZBZxjCjZDjZ
165 164 ralrimiva φxAZBZxjCjZDjZ
166 dfss3 AZBZjCjZDjZxAZBZxjCjZDjZ
167 165 166 sylibr φAZBZjCjZDjZ
168 eqidd φijCjZ=jCjZ
169 fveq2 j=iCj=Ci
170 169 fveq1d j=iCjZ=CiZ
171 170 adantl φij=iCjZ=CiZ
172 simpr φii
173 fvexd φiCiZV
174 168 171 172 173 fvmptd φijCjZi=CiZ
175 eqidd φijDjZ=jDjZ
176 fveq2 j=iDj=Di
177 176 fveq1d j=iDjZ=DiZ
178 177 adantl φij=iDjZ=DiZ
179 fvexd φiDiZV
180 175 178 172 179 fvmptd φijDjZi=DiZ
181 174 180 oveq12d φijCjZijDjZi=CiZDiZ
182 181 iuneq2dv φijCjZijDjZi=iCiZDiZ
183 170 177 oveq12d j=iCjZDjZ=CiZDiZ
184 183 cbviunv jCjZDjZ=iCiZDiZ
185 184 eqcomi iCiZDiZ=jCjZDjZ
186 185 a1i φiCiZDiZ=jCjZDjZ
187 182 186 eqtr2d φjCjZDjZ=ijCjZijDjZi
188 167 187 sseqtrd φAZBZijCjZijDjZi
189 188 ad2antrr φAZ<BZsum^jvolCjZDjZAZBZijCjZijDjZi
190 fvex CiZV
191 170 84 190 fvmpt ijCjZi=CiZ
192 fvex DiZV
193 177 87 192 fvmpt ijDjZi=DiZ
194 191 193 oveq12d ijCjZijDjZi=CiZDiZ
195 194 fveq2d ivoljCjZijDjZi=volCiZDiZ
196 195 mpteq2ia ivoljCjZijDjZi=ivolCiZDiZ
197 eqcom j=ii=j
198 197 imbi1i j=iCjZDjZ=CiZDiZi=jCjZDjZ=CiZDiZ
199 eqcom CjZDjZ=CiZDiZCiZDiZ=CjZDjZ
200 199 imbi2i i=jCjZDjZ=CiZDiZi=jCiZDiZ=CjZDjZ
201 198 200 bitri j=iCjZDjZ=CiZDiZi=jCiZDiZ=CjZDjZ
202 183 201 mpbi i=jCiZDiZ=CjZDjZ
203 202 fveq2d i=jvolCiZDiZ=volCjZDjZ
204 203 cbvmptv ivolCiZDiZ=jvolCjZDjZ
205 196 204 eqtri ivoljCjZijDjZi=jvolCjZDjZ
206 205 fveq2i sum^ivoljCjZijDjZi=sum^jvolCjZDjZ
207 206 a1i φAZ<BZsum^jvolCjZDjZsum^ivoljCjZijDjZi=sum^jvolCjZDjZ
208 simpr φAZ<BZsum^jvolCjZDjZsum^jvolCjZDjZ
209 207 208 eqeltrd φAZ<BZsum^jvolCjZDjZsum^ivoljCjZijDjZi
210 oveq1 w=zwAZ=zAZ
211 193 breq1d ijDjZizDiZz
212 211 193 ifbieq1d iifjDjZizjDjZiz=ifDiZzDiZz
213 191 212 oveq12d ijCjZiifjDjZizjDjZiz=CiZifDiZzDiZz
214 213 fveq2d ivoljCjZiifjDjZizjDjZiz=volCiZifDiZzDiZz
215 214 mpteq2ia ivoljCjZiifjDjZizjDjZiz=ivolCiZifDiZzDiZz
216 fveq2 i=hCi=Ch
217 216 fveq1d i=hCiZ=ChZ
218 fveq2 i=hDi=Dh
219 218 fveq1d i=hDiZ=DhZ
220 219 breq1d i=hDiZzDhZz
221 220 219 ifbieq1d i=hifDiZzDiZz=ifDhZzDhZz
222 217 221 oveq12d i=hCiZifDiZzDiZz=ChZifDhZzDhZz
223 222 fveq2d i=hvolCiZifDiZzDiZz=volChZifDhZzDhZz
224 223 cbvmptv ivolCiZifDiZzDiZz=hvolChZifDhZzDhZz
225 215 224 eqtri ivoljCjZiifjDjZizjDjZiz=hvolChZifDhZzDhZz
226 225 a1i w=zivoljCjZiifjDjZizjDjZiz=hvolChZifDhZzDhZz
227 breq2 w=zDhZwDhZz
228 id w=zw=z
229 227 228 ifbieq2d w=zifDhZwDhZw=ifDhZzDhZz
230 229 eqcomd w=zifDhZzDhZz=ifDhZwDhZw
231 230 oveq2d w=zChZifDhZzDhZz=ChZifDhZwDhZw
232 231 fveq2d w=zvolChZifDhZzDhZz=volChZifDhZwDhZw
233 232 mpteq2dv w=zhvolChZifDhZzDhZz=hvolChZifDhZwDhZw
234 226 233 eqtr2d w=zhvolChZifDhZwDhZw=ivoljCjZiifjDjZizjDjZiz
235 234 fveq2d w=zsum^hvolChZifDhZwDhZw=sum^ivoljCjZiifjDjZizjDjZiz
236 210 235 breq12d w=zwAZsum^hvolChZifDhZwDhZwzAZsum^ivoljCjZiifjDjZizjDjZiz
237 236 cbvrabv wAZBZ|wAZsum^hvolChZifDhZwDhZw=zAZBZ|zAZsum^ivoljCjZiifjDjZizjDjZiz
238 eqid supwAZBZ|wAZsum^hvolChZifDhZwDhZw<=supwAZBZ|wAZsum^hvolChZifDhZwDhZw<
239 81 82 83 86 89 189 209 237 238 hoidmv1lelem3 φAZ<BZsum^jvolCjZDjZBZAZsum^ivoljCjZijDjZi
240 239 207 breqtrd φAZ<BZsum^jvolCjZDjZBZAZsum^jvolCjZDjZ
241 25 80 240 syl2anc φAZ<BZ¬sum^jvolCjZDjZ=+∞BZAZsum^jvolCjZDjZ
242 24 241 pm2.61dan φAZ<BZBZAZsum^jvolCjZDjZ
243 1 32 34 4 5 hoidmvn0val φALXB=kXvolAkBk
244 29 prodeq1d φkXvolAkBk=kZvolAkBk
245 volicore AZBZvolAZBZ
246 13 12 245 syl2anc φvolAZBZ
247 246 recnd φvolAZBZ
248 117 119 oveq12d k=ZAkBk=AZBZ
249 248 fveq2d k=ZvolAkBk=volAZBZ
250 249 prodsn ZVvolAZBZkZvolAkBk=volAZBZ
251 2 247 250 syl2anc φkZvolAkBk=volAZBZ
252 243 244 251 3eqtrd φALXB=volAZBZ
253 252 adantr φAZ<BZALXB=volAZBZ
254 volico AZBZvolAZBZ=ifAZ<BZBZAZ0
255 13 12 254 syl2anc φvolAZBZ=ifAZ<BZBZAZ0
256 255 adantr φAZ<BZvolAZBZ=ifAZ<BZBZAZ0
257 iftrue AZ<BZifAZ<BZBZAZ0=BZAZ
258 257 adantl φAZ<BZifAZ<BZBZAZ0=BZAZ
259 253 256 258 3eqtrd φAZ<BZALXB=BZAZ
260 59 fveq2d φsum^jCjLXDj=sum^jvolCjZDjZ
261 260 adantr φAZ<BZsum^jCjLXDj=sum^jvolCjZDjZ
262 259 261 breq12d φAZ<BZALXBsum^jCjLXDjBZAZsum^jvolCjZDjZ
263 242 262 mpbird φAZ<BZALXBsum^jCjLXDj
264 243 adantr φ¬AZ<BZALXB=kXvolAkBk
265 244 adantr φ¬AZ<BZkXvolAkBk=kZvolAkBk
266 251 adantr φ¬AZ<BZkZvolAkBk=volAZBZ
267 255 adantr φ¬AZ<BZvolAZBZ=ifAZ<BZBZAZ0
268 iffalse ¬AZ<BZifAZ<BZBZAZ0=0
269 268 adantl φ¬AZ<BZifAZ<BZBZAZ0=0
270 266 267 269 3eqtrd φ¬AZ<BZkZvolAkBk=0
271 264 265 270 3eqtrd φ¬AZ<BZALXB=0
272 27 a1i φV
273 272 76 sge0ge0 φ0sum^jCjLXDj
274 273 adantr φ¬AZ<BZ0sum^jCjLXDj
275 271 274 eqbrtrd φ¬AZ<BZALXBsum^jCjLXDj
276 263 275 pm2.61dan φALXBsum^jCjLXDj