Metamath Proof Explorer


Theorem hoidmvlelem4

Description: The dimensional volume of a multidimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Induction step of Lemma 115B of Fremlin1 p. 29, case nonempty interval and dimension of the space greater than 1 . (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem4.l L=xFinax,bxifx=0kxvolakbk
hoidmvlelem4.x φXFin
hoidmvlelem4.y φYX
hoidmvlelem4.n φY
hoidmvlelem4.z φZXY
hoidmvlelem4.w W=YZ
hoidmvlelem4.a φA:W
hoidmvlelem4.b φB:W
hoidmvlelem4.k φkWAk<Bk
hoidmvlelem4.c φC:W
hoidmvlelem4.d φD:W
hoidmvlelem4.r φsum^jCjLWDj
hoidmvlelem4.h H=xcWjWifjYcjifcjxcjx
hoidmvlelem4.14 G=AYLYBY
hoidmvlelem4.e φE+
hoidmvlelem4.u U=zAZBZ|GzAZ1+Esum^jCjLWHzDj
hoidmvlelem4.s S=supU<
hoidmvlelem4.i φeYfYgYhYkYekfkjkYgjkhjkeLYfsum^jgjLYhj
hoidmvlelem4.i2 φkWAkBkjkWCjkDjk
Assertion hoidmvlelem4 φALWB1+Esum^jCjLWDj

Proof

Step Hyp Ref Expression
1 hoidmvlelem4.l L=xFinax,bxifx=0kxvolakbk
2 hoidmvlelem4.x φXFin
3 hoidmvlelem4.y φYX
4 hoidmvlelem4.n φY
5 hoidmvlelem4.z φZXY
6 hoidmvlelem4.w W=YZ
7 hoidmvlelem4.a φA:W
8 hoidmvlelem4.b φB:W
9 hoidmvlelem4.k φkWAk<Bk
10 hoidmvlelem4.c φC:W
11 hoidmvlelem4.d φD:W
12 hoidmvlelem4.r φsum^jCjLWDj
13 hoidmvlelem4.h H=xcWjWifjYcjifcjxcjx
14 hoidmvlelem4.14 G=AYLYBY
15 hoidmvlelem4.e φE+
16 hoidmvlelem4.u U=zAZBZ|GzAZ1+Esum^jCjLWHzDj
17 hoidmvlelem4.s S=supU<
18 hoidmvlelem4.i φeYfYgYhYkYekfkjkYgjkhjkeLYfsum^jgjLYhj
19 hoidmvlelem4.i2 φkWAkBkjkWCjkDjk
20 rge0ssre 0+∞
21 5 eldifad φZX
22 snssi ZXZX
23 21 22 syl φZX
24 3 23 unssd φYZX
25 6 24 eqsstrid φWX
26 ssfi XFinWXWFin
27 2 25 26 syl2anc φWFin
28 1 27 7 8 hoidmvcl φALWB0+∞
29 20 28 sselid φALWB
30 1red φ1
31 15 rpred φE
32 30 31 readdcld φ1+E
33 nfv jφ
34 nnex V
35 34 a1i φV
36 icossicc 0+∞0+∞
37 27 adantr φjWFin
38 10 ffvelrnda φjCjW
39 elmapi CjWCj:W
40 38 39 syl φjCj:W
41 eleq1 j=hjYhY
42 fveq2 j=hcj=ch
43 42 breq1d j=hcjxchx
44 43 42 ifbieq1d j=hifcjxcjx=ifchxchx
45 41 42 44 ifbieq12d j=hifjYcjifcjxcjx=ifhYchifchxchx
46 45 cbvmptv jWifjYcjifcjxcjx=hWifhYchifchxchx
47 46 mpteq2i cWjWifjYcjifcjxcjx=cWhWifhYchifchxchx
48 47 mpteq2i xcWjWifjYcjifcjxcjx=xcWhWifhYchifchxchx
49 13 48 eqtri H=xcWhWifhYchifchxchx
50 snidg ZXYZZ
51 5 50 syl φZZ
52 elun2 ZZZYZ
53 51 52 syl φZYZ
54 6 a1i φW=YZ
55 54 eqcomd φYZ=W
56 53 55 eleqtrd φZW
57 8 56 ffvelrnd φBZ
58 57 adantr φjBZ
59 11 ffvelrnda φjDjW
60 elmapi DjWDj:W
61 59 60 syl φjDj:W
62 49 58 37 61 hsphoif φjHBZDj:W
63 1 37 40 62 hoidmvcl φjCjLWHBZDj0+∞
64 36 63 sselid φjCjLWHBZDj0+∞
65 33 35 64 sge0clmpt φsum^jCjLWHBZDj0+∞
66 33 35 64 sge0xrclmpt φsum^jCjLWHBZDj*
67 pnfxr +∞*
68 67 a1i φ+∞*
69 12 rexrd φsum^jCjLWDj*
70 1 37 40 61 hoidmvcl φjCjLWDj0+∞
71 36 70 sselid φjCjLWDj0+∞
72 5 eldifbd φ¬ZY
73 56 72 eldifd φZWY
74 73 adantr φjZWY
75 1 37 74 6 58 49 40 61 hsphoidmvle φjCjLWHBZDjCjLWDj
76 33 35 64 71 75 sge0lempt φsum^jCjLWHBZDjsum^jCjLWDj
77 12 ltpnfd φsum^jCjLWDj<+∞
78 66 69 68 76 77 xrlelttrd φsum^jCjLWHBZDj<+∞
79 66 68 78 xrltned φsum^jCjLWHBZDj+∞
80 ge0xrre sum^jCjLWHBZDj0+∞sum^jCjLWHBZDj+∞sum^jCjLWHBZDj
81 65 79 80 syl2anc φsum^jCjLWHBZDj
82 32 81 remulcld φ1+Esum^jCjLWHBZDj
83 32 12 remulcld φ1+Esum^jCjLWDj
84 56 ancli φφZW
85 eleq1 k=ZkWZW
86 85 anbi2d k=ZφkWφZW
87 fveq2 k=ZAk=AZ
88 fveq2 k=ZBk=BZ
89 87 88 breq12d k=ZAk<BkAZ<BZ
90 86 89 imbi12d k=ZφkWAk<BkφZWAZ<BZ
91 90 9 vtoclg ZWφZWAZ<BZ
92 56 84 91 sylc φAZ<BZ
93 1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92 hoidmvlelem1 φSU
94 57 rexrd φBZ*
95 iccssxr AZBZ*
96 ssrab2 zAZBZ|GzAZ1+Esum^jCjLWHzDjAZBZ
97 16 96 eqsstri UAZBZ
98 97 93 sselid φSAZBZ
99 95 98 sselid φS*
100 simpl φ¬BZSφ
101 simpr φ¬BZS¬BZS
102 7 56 ffvelrnd φAZ
103 102 57 iccssred φAZBZ
104 103 98 sseldd φS
105 104 adantr φ¬BZSS
106 100 57 syl φ¬BZSBZ
107 105 106 ltnled φ¬BZSS<BZ¬BZS
108 101 107 mpbird φ¬BZSS<BZ
109 2 adantr φS<BZXFin
110 3 adantr φS<BZYX
111 5 adantr φS<BZZXY
112 7 adantr φS<BZA:W
113 8 adantr φS<BZB:W
114 9 adantlr φS<BZkWAk<Bk
115 eqid yY0=yY0
116 10 adantr φS<BZC:W
117 fveq2 i=jCi=Cj
118 117 fveq1d i=jCiZ=CjZ
119 fveq2 i=jDi=Dj
120 119 fveq1d i=jDiZ=DjZ
121 118 120 oveq12d i=jCiZDiZ=CjZDjZ
122 121 eleq2d i=jSCiZDiZSCjZDjZ
123 117 reseq1d i=jCiY=CjY
124 122 123 ifbieq1d i=jifSCiZDiZCiYyY0=ifSCjZDjZCjYyY0
125 124 cbvmptv iifSCiZDiZCiYyY0=jifSCjZDjZCjYyY0
126 11 adantr φS<BZD:W
127 119 reseq1d i=jDiY=DjY
128 122 127 ifbieq1d i=jifSCiZDiZDiYyY0=ifSCjZDjZDjYyY0
129 128 cbvmptv iifSCiZDiZDiYyY0=jifSCjZDjZDjYyY0
130 12 adantr φS<BZsum^jCjLWDj
131 15 adantr φS<BZE+
132 93 adantr φS<BZSU
133 simpr φS<BZS<BZ
134 biid SCiZDiZSCiZDiZ
135 eqidd w=y0=0
136 135 cbvmptv wY0=yY0
137 134 136 ifbieq2i ifSCiZDiZCiYwY0=ifSCiZDiZCiYyY0
138 137 mpteq2i iifSCiZDiZCiYwY0=iifSCiZDiZCiYyY0
139 138 a1i l=jiifSCiZDiZCiYwY0=iifSCiZDiZCiYyY0
140 id l=jl=j
141 139 140 fveq12d l=jiifSCiZDiZCiYwY0l=iifSCiZDiZCiYyY0j
142 134 136 ifbieq2i ifSCiZDiZDiYwY0=ifSCiZDiZDiYyY0
143 142 mpteq2i iifSCiZDiZDiYwY0=iifSCiZDiZDiYyY0
144 143 a1i l=jiifSCiZDiZDiYwY0=iifSCiZDiZDiYyY0
145 144 140 fveq12d l=jiifSCiZDiZDiYwY0l=iifSCiZDiZDiYyY0j
146 141 145 oveq12d l=jiifSCiZDiZCiYwY0lLYiifSCiZDiZDiYwY0l=iifSCiZDiZCiYyY0jLYiifSCiZDiZDiYyY0j
147 146 cbvmptv liifSCiZDiZCiYwY0lLYiifSCiZDiZDiYwY0l=jiifSCiZDiZCiYyY0jLYiifSCiZDiZDiYyY0j
148 18 adantr φS<BZeYfYgYhYkYekfkjkYgjkhjkeLYfsum^jgjLYhj
149 19 adantr φS<BZkWAkBkjkWCjkDjk
150 eqid xyYAyByyWifyYxyS=xyYAyByyWifyYxyS
151 fveq2 y=kAy=Ak
152 fveq2 y=kBy=Bk
153 151 152 oveq12d y=kAyBy=AkBk
154 153 cbvixpv yYAyBy=kYAkBk
155 eleq1 y=kyYkY
156 fveq2 y=kxy=xk
157 155 156 ifbieq1d y=kifyYxyS=ifkYxkS
158 157 cbvmptv yWifyYxyS=kWifkYxkS
159 154 158 mpteq12i xyYAyByyWifyYxyS=xkYAkBkkWifkYxkS
160 150 159 eqtri xyYAyByyWifyYxyS=xkYAkBkkWifkYxkS
161 1 109 110 111 6 112 113 114 115 116 125 126 129 130 13 14 131 16 132 133 147 148 149 160 hoidmvlelem3 φS<BZuUS<u
162 100 108 161 syl2anc φ¬BZSuUS<u
163 97 a1i φUAZBZ
164 163 103 sstrd φU
165 164 adantr φuUU
166 ne0i uUU
167 166 adantl φuUU
168 102 rexrd φAZ*
169 168 adantr φuUAZ*
170 94 adantr φuUBZ*
171 163 sselda φuUuAZBZ
172 iccleub AZ*BZ*uAZBZuBZ
173 169 170 171 172 syl3anc φuUuBZ
174 173 ralrimiva φuUuBZ
175 brralrspcev BZuUuBZyuUuy
176 57 174 175 syl2anc φyuUuy
177 176 adantr φuUyuUuy
178 simpr φuUuU
179 suprub UUyuUuyuUusupU<
180 165 167 177 178 179 syl31anc φuUusupU<
181 180 17 breqtrrdi φuUuS
182 181 ralrimiva φuUuS
183 165 178 sseldd φuUu
184 104 adantr φuUS
185 183 184 lenltd φuUuS¬S<u
186 185 ralbidva φuUuSuU¬S<u
187 182 186 mpbid φuU¬S<u
188 ralnex uU¬S<u¬uUS<u
189 187 188 sylib φ¬uUS<u
190 189 adantr φS<BZ¬uUS<u
191 100 108 190 syl2anc φ¬BZS¬uUS<u
192 162 191 condan φBZS
193 iccleub AZ*BZ*SAZBZSBZ
194 168 94 98 193 syl3anc φSBZ
195 94 99 192 194 xrletrid φBZ=S
196 16 eqcomi zAZBZ|GzAZ1+Esum^jCjLWHzDj=U
197 196 a1i φzAZBZ|GzAZ1+Esum^jCjLWHzDj=U
198 195 197 eleq12d φBZzAZBZ|GzAZ1+Esum^jCjLWHzDjSU
199 93 198 mpbird φBZzAZBZ|GzAZ1+Esum^jCjLWHzDj
200 oveq1 z=BZzAZ=BZAZ
201 200 oveq2d z=BZGzAZ=GBZAZ
202 fveq2 z=BZHz=HBZ
203 202 fveq1d z=BZHzDj=HBZDj
204 203 oveq2d z=BZCjLWHzDj=CjLWHBZDj
205 204 mpteq2dv z=BZjCjLWHzDj=jCjLWHBZDj
206 205 fveq2d z=BZsum^jCjLWHzDj=sum^jCjLWHBZDj
207 206 oveq2d z=BZ1+Esum^jCjLWHzDj=1+Esum^jCjLWHBZDj
208 201 207 breq12d z=BZGzAZ1+Esum^jCjLWHzDjGBZAZ1+Esum^jCjLWHBZDj
209 208 elrab BZzAZBZ|GzAZ1+Esum^jCjLWHzDjBZAZBZGBZAZ1+Esum^jCjLWHBZDj
210 199 209 sylib φBZAZBZGBZAZ1+Esum^jCjLWHBZDj
211 210 simprd φGBZAZ1+Esum^jCjLWHBZDj
212 2 3 ssfid φYFin
213 eqid kYvolAkBk=kYvolAkBk
214 1 212 5 72 6 7 8 213 hoiprodp1 φALWB=kYvolAkBkvolAZBZ
215 eqidd φkYBkAk=kYBkAk
216 7 adantr φkYA:W
217 ssun1 YYZ
218 6 eqcomi YZ=W
219 217 218 sseqtri YW
220 simpr φkYkY
221 219 220 sselid φkYkW
222 216 221 ffvelrnd φkYAk
223 8 adantr φkYB:W
224 223 221 ffvelrnd φkYBk
225 221 9 syldan φkYAk<Bk
226 222 224 225 volicon0 φkYvolAkBk=BkAk
227 226 prodeq2dv φkYvolAkBk=kYBkAk
228 14 a1i φG=AYLYBY
229 219 a1i φYW
230 7 229 fssresd φAY:Y
231 8 229 fssresd φBY:Y
232 1 212 4 230 231 hoidmvn0val φAYLYBY=kYvolAYkBYk
233 fvres kYAYk=Ak
234 fvres kYBYk=Bk
235 233 234 oveq12d kYAYkBYk=AkBk
236 235 fveq2d kYvolAYkBYk=volAkBk
237 236 adantl φkYvolAYkBYk=volAkBk
238 volico AkBkvolAkBk=ifAk<BkBkAk0
239 222 224 238 syl2anc φkYvolAkBk=ifAk<BkBkAk0
240 239 226 eqtr3d φkYifAk<BkBkAk0=BkAk
241 237 239 240 3eqtrd φkYvolAYkBYk=BkAk
242 241 prodeq2dv φkYvolAYkBYk=kYBkAk
243 228 232 242 3eqtrd φG=kYBkAk
244 215 227 243 3eqtr4d φkYvolAkBk=G
245 102 57 92 volicon0 φvolAZBZ=BZAZ
246 244 245 oveq12d φkYvolAkBkvolAZBZ=GBZAZ
247 214 246 eqtrd φALWB=GBZAZ
248 247 breq1d φALWB1+Esum^jCjLWHBZDjGBZAZ1+Esum^jCjLWHBZDj
249 211 248 mpbird φALWB1+Esum^jCjLWHBZDj
250 0le1 01
251 250 a1i φ01
252 15 rpge0d φ0E
253 30 31 251 252 addge0d φ01+E
254 81 12 32 253 76 lemul2ad φ1+Esum^jCjLWHBZDj1+Esum^jCjLWDj
255 29 82 83 249 254 letrd φALWB1+Esum^jCjLWDj