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 = x Fin a x , b x if x = 0 k x vol a k b k
hoidmvlelem4.x φ X Fin
hoidmvlelem4.y φ Y X
hoidmvlelem4.n φ Y
hoidmvlelem4.z φ Z X Y
hoidmvlelem4.w W = Y Z
hoidmvlelem4.a φ A : W
hoidmvlelem4.b φ B : W
hoidmvlelem4.k φ k W A k < B k
hoidmvlelem4.c φ C : W
hoidmvlelem4.d φ D : W
hoidmvlelem4.r φ sum^ j C j L W D j
hoidmvlelem4.h H = x c W j W if j Y c j if c j x c j x
hoidmvlelem4.14 G = A Y L Y B Y
hoidmvlelem4.e φ E +
hoidmvlelem4.u U = z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j
hoidmvlelem4.s S = sup U <
hoidmvlelem4.i φ e Y f Y g Y h Y k Y e k f k j k Y g j k h j k e L Y f sum^ j g j L Y h j
hoidmvlelem4.i2 φ k W A k B k j k W C j k D j k
Assertion hoidmvlelem4 φ A L W B 1 + E sum^ j C j L W D j

Proof

Step Hyp Ref Expression
1 hoidmvlelem4.l L = x Fin a x , b x if x = 0 k x vol a k b k
2 hoidmvlelem4.x φ X Fin
3 hoidmvlelem4.y φ Y X
4 hoidmvlelem4.n φ Y
5 hoidmvlelem4.z φ Z X Y
6 hoidmvlelem4.w W = Y Z
7 hoidmvlelem4.a φ A : W
8 hoidmvlelem4.b φ B : W
9 hoidmvlelem4.k φ k W A k < B k
10 hoidmvlelem4.c φ C : W
11 hoidmvlelem4.d φ D : W
12 hoidmvlelem4.r φ sum^ j C j L W D j
13 hoidmvlelem4.h H = x c W j W if j Y c j if c j x c j x
14 hoidmvlelem4.14 G = A Y L Y B Y
15 hoidmvlelem4.e φ E +
16 hoidmvlelem4.u U = z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j
17 hoidmvlelem4.s S = sup U <
18 hoidmvlelem4.i φ e Y f Y g Y h Y k Y e k f k j k Y g j k h j k e L Y f sum^ j g j L Y h j
19 hoidmvlelem4.i2 φ k W A k B k j k W C j k D j k
20 rge0ssre 0 +∞
21 5 eldifad φ Z X
22 snssi Z X Z X
23 21 22 syl φ Z X
24 3 23 unssd φ Y Z X
25 6 24 eqsstrid φ W X
26 ssfi X Fin W X W Fin
27 2 25 26 syl2anc φ W Fin
28 1 27 7 8 hoidmvcl φ A L W B 0 +∞
29 20 28 sselid φ A L W B
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 φ j W Fin
38 10 ffvelrnda φ j C j W
39 elmapi C j W C j : W
40 38 39 syl φ j C j : W
41 eleq1 j = h j Y h Y
42 fveq2 j = h c j = c h
43 42 breq1d j = h c j x c h x
44 43 42 ifbieq1d j = h if c j x c j x = if c h x c h x
45 41 42 44 ifbieq12d j = h if j Y c j if c j x c j x = if h Y c h if c h x c h x
46 45 cbvmptv j W if j Y c j if c j x c j x = h W if h Y c h if c h x c h x
47 46 mpteq2i c W j W if j Y c j if c j x c j x = c W h W if h Y c h if c h x c h x
48 47 mpteq2i x c W j W if j Y c j if c j x c j x = x c W h W if h Y c h if c h x c h x
49 13 48 eqtri H = x c W h W if h Y c h if c h x c h x
50 snidg Z X Y Z Z
51 5 50 syl φ Z Z
52 elun2 Z Z Z Y Z
53 51 52 syl φ Z Y Z
54 6 a1i φ W = Y Z
55 54 eqcomd φ Y Z = W
56 53 55 eleqtrd φ Z W
57 8 56 ffvelrnd φ B Z
58 57 adantr φ j B Z
59 11 ffvelrnda φ j D j W
60 elmapi D j W D j : W
61 59 60 syl φ j D j : W
62 49 58 37 61 hsphoif φ j H B Z D j : W
63 1 37 40 62 hoidmvcl φ j C j L W H B Z D j 0 +∞
64 36 63 sselid φ j C j L W H B Z D j 0 +∞
65 33 35 64 sge0clmpt φ sum^ j C j L W H B Z D j 0 +∞
66 33 35 64 sge0xrclmpt φ sum^ j C j L W H B Z D j *
67 pnfxr +∞ *
68 67 a1i φ +∞ *
69 12 rexrd φ sum^ j C j L W D j *
70 1 37 40 61 hoidmvcl φ j C j L W D j 0 +∞
71 36 70 sselid φ j C j L W D j 0 +∞
72 5 eldifbd φ ¬ Z Y
73 56 72 eldifd φ Z W Y
74 73 adantr φ j Z W Y
75 1 37 74 6 58 49 40 61 hsphoidmvle φ j C j L W H B Z D j C j L W D j
76 33 35 64 71 75 sge0lempt φ sum^ j C j L W H B Z D j sum^ j C j L W D j
77 12 ltpnfd φ sum^ j C j L W D j < +∞
78 66 69 68 76 77 xrlelttrd φ sum^ j C j L W H B Z D j < +∞
79 66 68 78 xrltned φ sum^ j C j L W H B Z D j +∞
80 ge0xrre sum^ j C j L W H B Z D j 0 +∞ sum^ j C j L W H B Z D j +∞ sum^ j C j L W H B Z D j
81 65 79 80 syl2anc φ sum^ j C j L W H B Z D j
82 32 81 remulcld φ 1 + E sum^ j C j L W H B Z D j
83 32 12 remulcld φ 1 + E sum^ j C j L W D j
84 56 ancli φ φ Z W
85 eleq1 k = Z k W Z W
86 85 anbi2d k = Z φ k W φ Z W
87 fveq2 k = Z A k = A Z
88 fveq2 k = Z B k = B Z
89 87 88 breq12d k = Z A k < B k A Z < B Z
90 86 89 imbi12d k = Z φ k W A k < B k φ Z W A Z < B Z
91 90 9 vtoclg Z W φ Z W A Z < B Z
92 56 84 91 sylc φ A Z < B Z
93 1 2 3 5 6 7 8 10 11 12 13 14 15 16 17 92 hoidmvlelem1 φ S U
94 57 rexrd φ B Z *
95 iccssxr A Z B Z *
96 ssrab2 z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j A Z B Z
97 16 96 eqsstri U A Z B Z
98 97 93 sselid φ S A Z B Z
99 95 98 sselid φ S *
100 simpl φ ¬ B Z S φ
101 simpr φ ¬ B Z S ¬ B Z S
102 7 56 ffvelrnd φ A Z
103 102 57 iccssred φ A Z B Z
104 103 98 sseldd φ S
105 104 adantr φ ¬ B Z S S
106 100 57 syl φ ¬ B Z S B Z
107 105 106 ltnled φ ¬ B Z S S < B Z ¬ B Z S
108 101 107 mpbird φ ¬ B Z S S < B Z
109 2 adantr φ S < B Z X Fin
110 3 adantr φ S < B Z Y X
111 5 adantr φ S < B Z Z X Y
112 7 adantr φ S < B Z A : W
113 8 adantr φ S < B Z B : W
114 9 adantlr φ S < B Z k W A k < B k
115 eqid y Y 0 = y Y 0
116 10 adantr φ S < B Z C : W
117 fveq2 i = j C i = C j
118 117 fveq1d i = j C i Z = C j Z
119 fveq2 i = j D i = D j
120 119 fveq1d i = j D i Z = D j Z
121 118 120 oveq12d i = j C i Z D i Z = C j Z D j Z
122 121 eleq2d i = j S C i Z D i Z S C j Z D j Z
123 117 reseq1d i = j C i Y = C j Y
124 122 123 ifbieq1d i = j if S C i Z D i Z C i Y y Y 0 = if S C j Z D j Z C j Y y Y 0
125 124 cbvmptv i if S C i Z D i Z C i Y y Y 0 = j if S C j Z D j Z C j Y y Y 0
126 11 adantr φ S < B Z D : W
127 119 reseq1d i = j D i Y = D j Y
128 122 127 ifbieq1d i = j if S C i Z D i Z D i Y y Y 0 = if S C j Z D j Z D j Y y Y 0
129 128 cbvmptv i if S C i Z D i Z D i Y y Y 0 = j if S C j Z D j Z D j Y y Y 0
130 12 adantr φ S < B Z sum^ j C j L W D j
131 15 adantr φ S < B Z E +
132 93 adantr φ S < B Z S U
133 simpr φ S < B Z S < B Z
134 biid S C i Z D i Z S C i Z D i Z
135 eqidd w = y 0 = 0
136 135 cbvmptv w Y 0 = y Y 0
137 134 136 ifbieq2i if S C i Z D i Z C i Y w Y 0 = if S C i Z D i Z C i Y y Y 0
138 137 mpteq2i i if S C i Z D i Z C i Y w Y 0 = i if S C i Z D i Z C i Y y Y 0
139 138 a1i l = j i if S C i Z D i Z C i Y w Y 0 = i if S C i Z D i Z C i Y y Y 0
140 id l = j l = j
141 139 140 fveq12d l = j i if S C i Z D i Z C i Y w Y 0 l = i if S C i Z D i Z C i Y y Y 0 j
142 134 136 ifbieq2i if S C i Z D i Z D i Y w Y 0 = if S C i Z D i Z D i Y y Y 0
143 142 mpteq2i i if S C i Z D i Z D i Y w Y 0 = i if S C i Z D i Z D i Y y Y 0
144 143 a1i l = j i if S C i Z D i Z D i Y w Y 0 = i if S C i Z D i Z D i Y y Y 0
145 144 140 fveq12d l = j i if S C i Z D i Z D i Y w Y 0 l = i if S C i Z D i Z D i Y y Y 0 j
146 141 145 oveq12d l = j i if S C i Z D i Z C i Y w Y 0 l L Y i if S C i Z D i Z D i Y w Y 0 l = i if S C i Z D i Z C i Y y Y 0 j L Y i if S C i Z D i Z D i Y y Y 0 j
147 146 cbvmptv l i if S C i Z D i Z C i Y w Y 0 l L Y i if S C i Z D i Z D i Y w Y 0 l = j i if S C i Z D i Z C i Y y Y 0 j L Y i if S C i Z D i Z D i Y y Y 0 j
148 18 adantr φ S < B Z e Y f Y g Y h Y k Y e k f k j k Y g j k h j k e L Y f sum^ j g j L Y h j
149 19 adantr φ S < B Z k W A k B k j k W C j k D j k
150 eqid x y Y A y B y y W if y Y x y S = x y Y A y B y y W if y Y x y S
151 fveq2 y = k A y = A k
152 fveq2 y = k B y = B k
153 151 152 oveq12d y = k A y B y = A k B k
154 153 cbvixpv y Y A y B y = k Y A k B k
155 eleq1 y = k y Y k Y
156 fveq2 y = k x y = x k
157 155 156 ifbieq1d y = k if y Y x y S = if k Y x k S
158 157 cbvmptv y W if y Y x y S = k W if k Y x k S
159 154 158 mpteq12i x y Y A y B y y W if y Y x y S = x k Y A k B k k W if k Y x k S
160 150 159 eqtri x y Y A y B y y W if y Y x y S = x k Y A k B k k W if k Y x k S
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 < B Z u U S < u
162 100 108 161 syl2anc φ ¬ B Z S u U S < u
163 97 a1i φ U A Z B Z
164 163 103 sstrd φ U
165 164 adantr φ u U U
166 ne0i u U U
167 166 adantl φ u U U
168 102 rexrd φ A Z *
169 168 adantr φ u U A Z *
170 94 adantr φ u U B Z *
171 163 sselda φ u U u A Z B Z
172 iccleub A Z * B Z * u A Z B Z u B Z
173 169 170 171 172 syl3anc φ u U u B Z
174 173 ralrimiva φ u U u B Z
175 brralrspcev B Z u U u B Z y u U u y
176 57 174 175 syl2anc φ y u U u y
177 176 adantr φ u U y u U u y
178 simpr φ u U u U
179 suprub U U y u U u y u U u sup U <
180 165 167 177 178 179 syl31anc φ u U u sup U <
181 180 17 breqtrrdi φ u U u S
182 181 ralrimiva φ u U u S
183 165 178 sseldd φ u U u
184 104 adantr φ u U S
185 183 184 lenltd φ u U u S ¬ S < u
186 185 ralbidva φ u U u S u U ¬ S < u
187 182 186 mpbid φ u U ¬ S < u
188 ralnex u U ¬ S < u ¬ u U S < u
189 187 188 sylib φ ¬ u U S < u
190 189 adantr φ S < B Z ¬ u U S < u
191 100 108 190 syl2anc φ ¬ B Z S ¬ u U S < u
192 162 191 condan φ B Z S
193 iccleub A Z * B Z * S A Z B Z S B Z
194 168 94 98 193 syl3anc φ S B Z
195 94 99 192 194 xrletrid φ B Z = S
196 16 eqcomi z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j = U
197 196 a1i φ z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j = U
198 195 197 eleq12d φ B Z z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j S U
199 93 198 mpbird φ B Z z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j
200 oveq1 z = B Z z A Z = B Z A Z
201 200 oveq2d z = B Z G z A Z = G B Z A Z
202 fveq2 z = B Z H z = H B Z
203 202 fveq1d z = B Z H z D j = H B Z D j
204 203 oveq2d z = B Z C j L W H z D j = C j L W H B Z D j
205 204 mpteq2dv z = B Z j C j L W H z D j = j C j L W H B Z D j
206 205 fveq2d z = B Z sum^ j C j L W H z D j = sum^ j C j L W H B Z D j
207 206 oveq2d z = B Z 1 + E sum^ j C j L W H z D j = 1 + E sum^ j C j L W H B Z D j
208 201 207 breq12d z = B Z G z A Z 1 + E sum^ j C j L W H z D j G B Z A Z 1 + E sum^ j C j L W H B Z D j
209 208 elrab B Z z A Z B Z | G z A Z 1 + E sum^ j C j L W H z D j B Z A Z B Z G B Z A Z 1 + E sum^ j C j L W H B Z D j
210 199 209 sylib φ B Z A Z B Z G B Z A Z 1 + E sum^ j C j L W H B Z D j
211 210 simprd φ G B Z A Z 1 + E sum^ j C j L W H B Z D j
212 2 3 ssfid φ Y Fin
213 eqid k Y vol A k B k = k Y vol A k B k
214 1 212 5 72 6 7 8 213 hoiprodp1 φ A L W B = k Y vol A k B k vol A Z B Z
215 eqidd φ k Y B k A k = k Y B k A k
216 7 adantr φ k Y A : W
217 ssun1 Y Y Z
218 6 eqcomi Y Z = W
219 217 218 sseqtri Y W
220 simpr φ k Y k Y
221 219 220 sselid φ k Y k W
222 216 221 ffvelrnd φ k Y A k
223 8 adantr φ k Y B : W
224 223 221 ffvelrnd φ k Y B k
225 221 9 syldan φ k Y A k < B k
226 222 224 225 volicon0 φ k Y vol A k B k = B k A k
227 226 prodeq2dv φ k Y vol A k B k = k Y B k A k
228 14 a1i φ G = A Y L Y B Y
229 219 a1i φ Y W
230 7 229 fssresd φ A Y : Y
231 8 229 fssresd φ B Y : Y
232 1 212 4 230 231 hoidmvn0val φ A Y L Y B Y = k Y vol A Y k B Y k
233 fvres k Y A Y k = A k
234 fvres k Y B Y k = B k
235 233 234 oveq12d k Y A Y k B Y k = A k B k
236 235 fveq2d k Y vol A Y k B Y k = vol A k B k
237 236 adantl φ k Y vol A Y k B Y k = vol A k B k
238 volico A k B k vol A k B k = if A k < B k B k A k 0
239 222 224 238 syl2anc φ k Y vol A k B k = if A k < B k B k A k 0
240 239 226 eqtr3d φ k Y if A k < B k B k A k 0 = B k A k
241 237 239 240 3eqtrd φ k Y vol A Y k B Y k = B k A k
242 241 prodeq2dv φ k Y vol A Y k B Y k = k Y B k A k
243 228 232 242 3eqtrd φ G = k Y B k A k
244 215 227 243 3eqtr4d φ k Y vol A k B k = G
245 102 57 92 volicon0 φ vol A Z B Z = B Z A Z
246 244 245 oveq12d φ k Y vol A k B k vol A Z B Z = G B Z A Z
247 214 246 eqtrd φ A L W B = G B Z A Z
248 247 breq1d φ A L W B 1 + E sum^ j C j L W H B Z D j G B Z A Z 1 + E sum^ j C j L W H B Z D j
249 211 248 mpbird φ A L W B 1 + E sum^ j C j L W H B Z D j
250 0le1 0 1
251 250 a1i φ 0 1
252 15 rpge0d φ 0 E
253 30 31 251 252 addge0d φ 0 1 + E
254 81 12 32 253 76 lemul2ad φ 1 + E sum^ j C j L W H B Z D j 1 + E sum^ j C j L W D j
255 29 82 83 249 254 letrd φ A L W B 1 + E sum^ j C j L W D j