Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  hoidmvle Structured version   Visualization version   Unicode version

Theorem hoidmvle 38540
 Description: The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
Hypotheses
Ref Expression
hoidmvle.l
hoidmvle.x
hoidmvle.a
hoidmvle.b
hoidmvle.c
hoidmvle.d
hoidmvle.s
Assertion
Ref Expression
hoidmvle Σ^
Distinct variable groups:   ,,,   ,,   ,,   ,,   ,,,,   ,,,,,   ,,,,
Allowed substitution hints:   ()   (,)   (,,)   (,,)   (,,)   ()

Proof of Theorem hoidmvle
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hoidmvle.s . 2
2 hoidmvle.d . . . 4
3 ovex 6336 . . . . . . 7
4 nnex 10637 . . . . . . 7
53, 4pm3.2i 462 . . . . . 6
65a1i 11 . . . . 5
7 elmapg 7503 . . . . 5
86, 7syl 17 . . . 4
92, 8mpbird 240 . . 3
10 hoidmvle.c . . . . 5
11 elmapg 7503 . . . . . 6
126, 11syl 17 . . . . 5
1310, 12mpbird 240 . . . 4
14 hoidmvle.b . . . . . 6
15 reex 9648 . . . . . . . . 9
1615a1i 11 . . . . . . . 8
17 hoidmvle.x . . . . . . . 8
1816, 17jca 541 . . . . . . 7
19 elmapg 7503 . . . . . . 7
2018, 19syl 17 . . . . . 6
2114, 20mpbird 240 . . . . 5
22 hoidmvle.a . . . . . . 7
23 elmapg 7503 . . . . . . . 8
2418, 23syl 17 . . . . . . 7
2522, 24mpbird 240 . . . . . 6
26 oveq2 6316 . . . . . . . . . 10
2726eleq2d 2534 . . . . . . . . 9
2826eleq2d 2534 . . . . . . . . . . 11
2926oveq1d 6323 . . . . . . . . . . . . . 14
3029eleq2d 2534 . . . . . . . . . . . . 13
3129eleq2d 2534 . . . . . . . . . . . . . . 15
32 ixpeq1 7551 . . . . . . . . . . . . . . . . 17
33 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18
3433iuneq2d 4296 . . . . . . . . . . . . . . . . 17
3532, 34sseq12d 3447 . . . . . . . . . . . . . . . 16
36 fveq2 5879 . . . . . . . . . . . . . . . . . 18
3736oveqd 6325 . . . . . . . . . . . . . . . . 17
3836oveqd 6325 . . . . . . . . . . . . . . . . . . 19
3938mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18
4039fveq2d 5883 . . . . . . . . . . . . . . . . 17 Σ^ Σ^
4137, 40breq12d 4408 . . . . . . . . . . . . . . . 16 Σ^ Σ^
4235, 41imbi12d 327 . . . . . . . . . . . . . . 15 Σ^ Σ^
4331, 42imbi12d 327 . . . . . . . . . . . . . 14 Σ^ Σ^
4443ralbidv2 2827 . . . . . . . . . . . . 13 Σ^ Σ^
4530, 44imbi12d 327 . . . . . . . . . . . 12 Σ^ Σ^
4645ralbidv2 2827 . . . . . . . . . . 11 Σ^ Σ^
4728, 46imbi12d 327 . . . . . . . . . 10 Σ^ Σ^
4847ralbidv2 2827 . . . . . . . . 9 Σ^ Σ^
4927, 48imbi12d 327 . . . . . . . 8 Σ^ Σ^
5049ralbidv2 2827 . . . . . . 7 Σ^ Σ^
51 oveq2 6316 . . . . . . . . . 10
5251eleq2d 2534 . . . . . . . . 9
5351eleq2d 2534 . . . . . . . . . . 11
5451oveq1d 6323 . . . . . . . . . . . . . 14
5554eleq2d 2534 . . . . . . . . . . . . 13
5654eleq2d 2534 . . . . . . . . . . . . . . 15
57 ixpeq1 7551 . . . . . . . . . . . . . . . . 17
58 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18
5958iuneq2d 4296 . . . . . . . . . . . . . . . . 17
6057, 59sseq12d 3447 . . . . . . . . . . . . . . . 16
61 fveq2 5879 . . . . . . . . . . . . . . . . . 18
6261oveqd 6325 . . . . . . . . . . . . . . . . 17
6361oveqd 6325 . . . . . . . . . . . . . . . . . . 19
6463mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18
6564fveq2d 5883 . . . . . . . . . . . . . . . . 17 Σ^ Σ^
6662, 65breq12d 4408 . . . . . . . . . . . . . . . 16 Σ^ Σ^
6760, 66imbi12d 327 . . . . . . . . . . . . . . 15 Σ^ Σ^
6856, 67imbi12d 327 . . . . . . . . . . . . . 14 Σ^ Σ^
6968ralbidv2 2827 . . . . . . . . . . . . 13 Σ^ Σ^
7055, 69imbi12d 327 . . . . . . . . . . . 12 Σ^ Σ^
7170ralbidv2 2827 . . . . . . . . . . 11 Σ^ Σ^
7253, 71imbi12d 327 . . . . . . . . . 10 Σ^ Σ^
7372ralbidv2 2827 . . . . . . . . 9 Σ^ Σ^
7452, 73imbi12d 327 . . . . . . . 8 Σ^ Σ^
7574ralbidv2 2827 . . . . . . 7 Σ^ Σ^
76 oveq2 6316 . . . . . . . . . 10
7776eleq2d 2534 . . . . . . . . 9
7876eleq2d 2534 . . . . . . . . . . 11
7976oveq1d 6323 . . . . . . . . . . . . . 14
8079eleq2d 2534 . . . . . . . . . . . . 13
8179eleq2d 2534 . . . . . . . . . . . . . . 15
82 ixpeq1 7551 . . . . . . . . . . . . . . . . 17
83 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18
8483iuneq2d 4296 . . . . . . . . . . . . . . . . 17
8582, 84sseq12d 3447 . . . . . . . . . . . . . . . 16
86 fveq2 5879 . . . . . . . . . . . . . . . . . 18
8786oveqd 6325 . . . . . . . . . . . . . . . . 17
8886oveqd 6325 . . . . . . . . . . . . . . . . . . 19
8988mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18
9089fveq2d 5883 . . . . . . . . . . . . . . . . 17 Σ^ Σ^
9187, 90breq12d 4408 . . . . . . . . . . . . . . . 16 Σ^ Σ^
9285, 91imbi12d 327 . . . . . . . . . . . . . . 15 Σ^ Σ^
9381, 92imbi12d 327 . . . . . . . . . . . . . 14 Σ^ Σ^
9493ralbidv2 2827 . . . . . . . . . . . . 13 Σ^ Σ^
9580, 94imbi12d 327 . . . . . . . . . . . 12 Σ^ Σ^
9695ralbidv2 2827 . . . . . . . . . . 11 Σ^ Σ^
9778, 96imbi12d 327 . . . . . . . . . 10 Σ^ Σ^
9897ralbidv2 2827 . . . . . . . . 9 Σ^ Σ^
9977, 98imbi12d 327 . . . . . . . 8 Σ^ Σ^
10099ralbidv2 2827 . . . . . . 7 Σ^ Σ^
101 oveq2 6316 . . . . . . . . . 10
102101eleq2d 2534 . . . . . . . . 9
103101eleq2d 2534 . . . . . . . . . . 11
104101oveq1d 6323 . . . . . . . . . . . . . 14
105104eleq2d 2534 . . . . . . . . . . . . 13
106104eleq2d 2534 . . . . . . . . . . . . . . 15
107 ixpeq1 7551 . . . . . . . . . . . . . . . . 17
108 ixpeq1 7551 . . . . . . . . . . . . . . . . . 18
109108iuneq2d 4296 . . . . . . . . . . . . . . . . 17
110107, 109sseq12d 3447 . . . . . . . . . . . . . . . 16
111 fveq2 5879 . . . . . . . . . . . . . . . . . 18
112111oveqd 6325 . . . . . . . . . . . . . . . . 17
113111oveqd 6325 . . . . . . . . . . . . . . . . . . 19
114113mpteq2dv 4483 . . . . . . . . . . . . . . . . . 18
115114fveq2d 5883 . . . . . . . . . . . . . . . . 17 Σ^ Σ^
116112, 115breq12d 4408 . . . . . . . . . . . . . . . 16 Σ^ Σ^
117110, 116imbi12d 327 . . . . . . . . . . . . . . 15 Σ^ Σ^
118106, 117imbi12d 327 . . . . . . . . . . . . . 14 Σ^ Σ^
119118ralbidv2 2827 . . . . . . . . . . . . 13 Σ^ Σ^
120105, 119imbi12d 327 . . . . . . . . . . . 12 Σ^ Σ^
121120ralbidv2 2827 . . . . . . . . . . 11 Σ^ Σ^
122103, 121imbi12d 327 . . . . . . . . . 10 Σ^ Σ^
123122ralbidv2 2827 . . . . . . . . 9 Σ^ Σ^
124102, 123imbi12d 327 . . . . . . . 8 Σ^ Σ^
125124ralbidv2 2827 . . . . . . 7 Σ^ Σ^
126 hoidmvle.l . . . . . . . . . . . . . . . 16
127 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . 22
128127oveq1d 6323 . . . . . . . . . . . . . . . . . . . . 21
129128fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
130129prodeq2ad 37769 . . . . . . . . . . . . . . . . . . 19
131130ifeq2d 3891 . . . . . . . . . . . . . . . . . 18
132 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . 22
133132oveq2d 6324 . . . . . . . . . . . . . . . . . . . . 21
134133fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20
135134prodeq2ad 37769 . . . . . . . . . . . . . . . . . . 19
136135ifeq2d 3891 . . . . . . . . . . . . . . . . . 18
137131, 136cbvmpt2v 6390 . . . . . . . . . . . . . . . . 17
138137mpteq2i 4479 . . . . . . . . . . . . . . . 16
139126, 138eqtri 2493 . . . . . . . . . . . . . . 15
140 elmapi 7511 . . . . . . . . . . . . . . . 16
141140adantr 472 . . . . . . . . . . . . . . 15
142 elmapi 7511 . . . . . . . . . . . . . . . 16
143142adantl 473 . . . . . . . . . . . . . . 15
144139, 141, 143hoidmv0val 38523 . . . . . . . . . . . . . 14
145144ad5ant23 1270 . . . . . . . . . . . . 13
146 nfv 1769 . . . . . . . . . . . . . . 15
1474a1i 11 . . . . . . . . . . . . . . 15
148 icossicc 11746 . . . . . . . . . . . . . . . 16
149 0fin 7817 . . . . . . . . . . . . . . . . . 18
150149a1i 11 . . . . . . . . . . . . . . . . 17
151 ovex 6336 . . . . . . . . . . . . . . . . . . . . 21
152151a1i 11 . . . . . . . . . . . . . . . . . . . 20
1534a1i 11 . . . . . . . . . . . . . . . . . . . 20
154 simpl 464 . . . . . . . . . . . . . . . . . . . 20
155 simpr 468 . . . . . . . . . . . . . . . . . . . 20
156152, 153, 154, 155fvmap 37546 . . . . . . . . . . . . . . . . . . 19
157 elmapi 7511 . . . . . . . . . . . . . . . . . . 19
158156, 157syl 17 . . . . . . . . . . . . . . . . . 18
159158adantlr 729 . . . . . . . . . . . . . . . . 17
160151a1i 11 . . . . . . . . . . . . . . . . . . . 20
1614a1i 11 . . . . . . . . . . . . . . . . . . . 20
162 simpl 464 . . . . . . . . . . . . . . . . . . . 20
163 simpr 468 . . . . . . . . . . . . . . . . . . . 20
164160, 161, 162, 163fvmap 37546 . . . . . . . . . . . . . . . . . . 19
165 elmapi 7511 . . . . . . . . . . . . . . . . . . 19
166164, 165syl 17 . . . . . . . . . . . . . . . . . 18
167166adantll 728 . . . . . . . . . . . . . . . . 17
168126, 150, 159, 167hoidmvcl 38522 . . . . . . . . . . . . . . . 16
169148, 168sseldi 3416 . . . . . . . . . . . . . . 15
170146, 147, 169sge0ge0mpt 38394 . . . . . . . . . . . . . 14 Σ^
171170adantll 728 . . . . . . . . . . . . 13 Σ^
172145, 171eqbrtrd 4416 . . . . . . . . . . . 12 Σ^
173172a1d 25 . . . . . . . . . . 11 Σ^
174173ralrimiva 2809 . . . . . . . . . 10 Σ^
175174ralrimiva 2809 . . . . . . . . 9 Σ^
176175ralrimiva 2809 . . . . . . . 8 Σ^
177176ralrimiva 2809 . . . . . . 7 Σ^
178 simpl 464 . . . . . . . . 9 Σ^
179128ixpeq2dv 7556 . . . . . . . . . . . . . . . . . 18
180179sseq1d 3445 . . . . . . . . . . . . . . . . 17
181 oveq1 6315 . . . . . . . . . . . . . . . . . 18
182181breq1d 4405 . . . . . . . . . . . . . . . . 17 Σ^ Σ^
183180, 182imbi12d 327 . . . . . . . . . . . . . . . 16 Σ^ Σ^
184183ralbidv 2829 . . . . . . . . . . . . . . 15 Σ^ Σ^
185184ralbidv 2829 . . . . . . . . . . . . . 14 Σ^ Σ^
186185ralbidv 2829 . . . . . . . . . . . . 13 Σ^ Σ^
187133ixpeq2dv 7556 . . . . . . . . . . . . . . . . . . . 20
188187sseq1d 3445 . . . . . . . . . . . . . . . . . . 19
189 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
190189breq1d 4405 . . . . . . . . . . . . . . . . . . 19 Σ^ Σ^
191188, 190imbi12d 327 . . . . . . . . . . . . . . . . . 18 Σ^ Σ^
192191ralbidv 2829 . . . . . . . . . . . . . . . . 17 Σ^