Metamath Proof Explorer


Theorem ovnhoilem2

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. Second part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoilem2.x φ X Fin
ovnhoilem2.n φ X
ovnhoilem2.a φ A : X
ovnhoilem2.b φ B : X
ovnhoilem2.i I = k X A k B k
ovnhoilem2.l L = x Fin a x , b x if x = 0 k x vol a k b k
ovnhoilem2.m M = z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k
ovnhoilem2.f F = i 2 X n l X 1 st i n l
ovnhoilem2.s S = i 2 X n l X 2 nd i n l
Assertion ovnhoilem2 φ A L X B voln* X I

Proof

Step Hyp Ref Expression
1 ovnhoilem2.x φ X Fin
2 ovnhoilem2.n φ X
3 ovnhoilem2.a φ A : X
4 ovnhoilem2.b φ B : X
5 ovnhoilem2.i I = k X A k B k
6 ovnhoilem2.l L = x Fin a x , b x if x = 0 k x vol a k b k
7 ovnhoilem2.m M = z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k
8 ovnhoilem2.f F = i 2 X n l X 1 st i n l
9 ovnhoilem2.s S = i 2 X n l X 2 nd i n l
10 7 eleq2i z M z z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k
11 rabid z z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k z * i 2 X I j k X . i j k z = sum^ j k X vol . i j k
12 10 11 bitri z M z * i 2 X I j k X . i j k z = sum^ j k X vol . i j k
13 12 biimpi z M z * i 2 X I j k X . i j k z = sum^ j k X vol . i j k
14 13 simprd z M i 2 X I j k X . i j k z = sum^ j k X vol . i j k
15 14 adantl φ z M i 2 X I j k X . i j k z = sum^ j k X vol . i j k
16 1 3ad2ant1 φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k X Fin
17 3 3ad2ant1 φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k A : X
18 4 3ad2ant1 φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k B : X
19 elmapi i 2 X i : 2 X
20 19 ffvelrnda i 2 X n i n 2 X
21 elmapi i n 2 X i n : X 2
22 20 21 syl i 2 X n i n : X 2
23 22 ffvelrnda i 2 X n l X i n l 2
24 xp1st i n l 2 1 st i n l
25 23 24 syl i 2 X n l X 1 st i n l
26 25 fmpttd i 2 X n l X 1 st i n l : X
27 reex V
28 27 a1i i 2 X n V
29 1nn 1
30 29 a1i i 2 X 1
31 19 30 ffvelrnd i 2 X i 1 2 X
32 elmapex i 1 2 X 2 V X V
33 32 simprd i 1 2 X X V
34 31 33 syl i 2 X X V
35 34 adantr i 2 X n X V
36 elmapg V X V l X 1 st i n l X l X 1 st i n l : X
37 28 35 36 syl2anc i 2 X n l X 1 st i n l X l X 1 st i n l : X
38 26 37 mpbird i 2 X n l X 1 st i n l X
39 38 fmpttd i 2 X n l X 1 st i n l : X
40 id i 2 X i 2 X
41 nnex V
42 41 mptex n l X 1 st i n l V
43 42 a1i i 2 X n l X 1 st i n l V
44 8 fvmpt2 i 2 X n l X 1 st i n l V F i = n l X 1 st i n l
45 40 43 44 syl2anc i 2 X F i = n l X 1 st i n l
46 45 feq1d i 2 X F i : X n l X 1 st i n l : X
47 39 46 mpbird i 2 X F i : X
48 47 3ad2ant2 φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k F i : X
49 xp2nd i n l 2 2 nd i n l
50 23 49 syl i 2 X n l X 2 nd i n l
51 50 fmpttd i 2 X n l X 2 nd i n l : X
52 elmapg V X V l X 2 nd i n l X l X 2 nd i n l : X
53 28 35 52 syl2anc i 2 X n l X 2 nd i n l X l X 2 nd i n l : X
54 51 53 mpbird i 2 X n l X 2 nd i n l X
55 54 fmpttd i 2 X n l X 2 nd i n l : X
56 41 mptex n l X 2 nd i n l V
57 56 a1i i 2 X n l X 2 nd i n l V
58 9 fvmpt2 i 2 X n l X 2 nd i n l V S i = n l X 2 nd i n l
59 40 57 58 syl2anc i 2 X S i = n l X 2 nd i n l
60 59 feq1d i 2 X S i : X n l X 2 nd i n l : X
61 55 60 mpbird i 2 X S i : X
62 61 3ad2ant2 φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k S i : X
63 simp3 φ i 2 X I j k X . i j k I j k X . i j k
64 5 a1i φ i 2 X I j k X . i j k I = k X A k B k
65 fveq2 j = n i j = i n
66 65 fveq1d j = n i j k = i n k
67 66 fveq2d j = n 1 st i j k = 1 st i n k
68 66 fveq2d j = n 2 nd i j k = 2 nd i n k
69 67 68 oveq12d j = n 1 st i j k 2 nd i j k = 1 st i n k 2 nd i n k
70 69 ixpeq2dv j = n k X 1 st i j k 2 nd i j k = k X 1 st i n k 2 nd i n k
71 70 cbviunv j k X 1 st i j k 2 nd i j k = n k X 1 st i n k 2 nd i n k
72 71 a1i i 2 X j k X 1 st i j k 2 nd i j k = n k X 1 st i n k 2 nd i n k
73 19 ffvelrnda i 2 X j i j 2 X
74 elmapi i j 2 X i j : X 2
75 73 74 syl i 2 X j i j : X 2
76 75 adantr i 2 X j k X i j : X 2
77 simpr i 2 X j k X k X
78 76 77 fvovco i 2 X j k X . i j k = 1 st i j k 2 nd i j k
79 78 ixpeq2dva i 2 X j k X . i j k = k X 1 st i j k 2 nd i j k
80 79 iuneq2dv i 2 X j k X . i j k = j k X 1 st i j k 2 nd i j k
81 simpl i 2 X n i 2 X
82 42 a1i i 2 X n n l X 1 st i n l V
83 81 82 44 syl2anc i 2 X n F i = n l X 1 st i n l
84 83 fveq1d i 2 X n F i n = n l X 1 st i n l n
85 simpr i 2 X n n
86 mptexg X V l X 1 st i n l V
87 34 86 syl i 2 X l X 1 st i n l V
88 87 adantr i 2 X n l X 1 st i n l V
89 eqid n l X 1 st i n l = n l X 1 st i n l
90 89 fvmpt2 n l X 1 st i n l V n l X 1 st i n l n = l X 1 st i n l
91 85 88 90 syl2anc i 2 X n n l X 1 st i n l n = l X 1 st i n l
92 84 91 eqtrd i 2 X n F i n = l X 1 st i n l
93 92 fveq1d i 2 X n F i n k = l X 1 st i n l k
94 93 adantr i 2 X n k X F i n k = l X 1 st i n l k
95 eqidd i 2 X k X l X 1 st i n l = l X 1 st i n l
96 simpr i 2 X k X l = k l = k
97 96 fveq2d i 2 X k X l = k i n l = i n k
98 97 fveq2d i 2 X k X l = k 1 st i n l = 1 st i n k
99 simpr i 2 X k X k X
100 fvexd i 2 X k X 1 st i n k V
101 95 98 99 100 fvmptd i 2 X k X l X 1 st i n l k = 1 st i n k
102 101 adantlr i 2 X n k X l X 1 st i n l k = 1 st i n k
103 94 102 eqtrd i 2 X n k X F i n k = 1 st i n k
104 59 fveq1d i 2 X S i n = n l X 2 nd i n l n
105 104 adantr i 2 X n S i n = n l X 2 nd i n l n
106 mptexg X V l X 2 nd i n l V
107 34 106 syl i 2 X l X 2 nd i n l V
108 107 adantr i 2 X n l X 2 nd i n l V
109 eqid n l X 2 nd i n l = n l X 2 nd i n l
110 109 fvmpt2 n l X 2 nd i n l V n l X 2 nd i n l n = l X 2 nd i n l
111 85 108 110 syl2anc i 2 X n n l X 2 nd i n l n = l X 2 nd i n l
112 105 111 eqtrd i 2 X n S i n = l X 2 nd i n l
113 112 fveq1d i 2 X n S i n k = l X 2 nd i n l k
114 113 adantr i 2 X n k X S i n k = l X 2 nd i n l k
115 eqidd i 2 X k X l X 2 nd i n l = l X 2 nd i n l
116 2fveq3 l = k 2 nd i n l = 2 nd i n k
117 116 adantl i 2 X k X l = k 2 nd i n l = 2 nd i n k
118 fvexd i 2 X k X 2 nd i n k V
119 115 117 99 118 fvmptd i 2 X k X l X 2 nd i n l k = 2 nd i n k
120 119 adantlr i 2 X n k X l X 2 nd i n l k = 2 nd i n k
121 114 120 eqtrd i 2 X n k X S i n k = 2 nd i n k
122 103 121 oveq12d i 2 X n k X F i n k S i n k = 1 st i n k 2 nd i n k
123 122 ixpeq2dva i 2 X n k X F i n k S i n k = k X 1 st i n k 2 nd i n k
124 123 iuneq2dv i 2 X n k X F i n k S i n k = n k X 1 st i n k 2 nd i n k
125 72 80 124 3eqtr4d i 2 X j k X . i j k = n k X F i n k S i n k
126 125 adantl φ i 2 X j k X . i j k = n k X F i n k S i n k
127 126 3adant3 φ i 2 X I j k X . i j k j k X . i j k = n k X F i n k S i n k
128 64 127 sseq12d φ i 2 X I j k X . i j k I j k X . i j k k X A k B k n k X F i n k S i n k
129 63 128 mpbid φ i 2 X I j k X . i j k k X A k B k n k X F i n k S i n k
130 129 3adant3r φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k k X A k B k n k X F i n k S i n k
131 6 16 17 18 48 62 130 hoidmvle φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k A L X B sum^ n F i n L X S i n
132 simpl n = j l X n = j
133 132 fveq2d n = j l X i n = i j
134 133 fveq1d n = j l X i n l = i j l
135 134 fveq2d n = j l X 1 st i n l = 1 st i j l
136 135 mpteq2dva n = j l X 1 st i n l = l X 1 st i j l
137 136 fveq1d n = j l X 1 st i n l k = l X 1 st i j l k
138 137 adantr n = j k X l X 1 st i n l k = l X 1 st i j l k
139 eqidd k X l X 1 st i j l = l X 1 st i j l
140 2fveq3 l = k 1 st i j l = 1 st i j k
141 140 adantl k X l = k 1 st i j l = 1 st i j k
142 id k X k X
143 fvexd k X 1 st i j k V
144 139 141 142 143 fvmptd k X l X 1 st i j l k = 1 st i j k
145 144 adantl n = j k X l X 1 st i j l k = 1 st i j k
146 138 145 eqtrd n = j k X l X 1 st i n l k = 1 st i j k
147 134 fveq2d n = j l X 2 nd i n l = 2 nd i j l
148 147 mpteq2dva n = j l X 2 nd i n l = l X 2 nd i j l
149 148 fveq1d n = j l X 2 nd i n l k = l X 2 nd i j l k
150 149 adantr n = j k X l X 2 nd i n l k = l X 2 nd i j l k
151 eqidd k X l X 2 nd i j l = l X 2 nd i j l
152 2fveq3 l = k 2 nd i j l = 2 nd i j k
153 152 adantl k X l = k 2 nd i j l = 2 nd i j k
154 fvexd k X 2 nd i j k V
155 151 153 142 154 fvmptd k X l X 2 nd i j l k = 2 nd i j k
156 155 adantl n = j k X l X 2 nd i j l k = 2 nd i j k
157 150 156 eqtrd n = j k X l X 2 nd i n l k = 2 nd i j k
158 146 157 oveq12d n = j k X l X 1 st i n l k l X 2 nd i n l k = 1 st i j k 2 nd i j k
159 158 fveq2d n = j k X vol l X 1 st i n l k l X 2 nd i n l k = vol 1 st i j k 2 nd i j k
160 159 prodeq2dv n = j k X vol l X 1 st i n l k l X 2 nd i n l k = k X vol 1 st i j k 2 nd i j k
161 160 cbvmptv n k X vol l X 1 st i n l k l X 2 nd i n l k = j k X vol 1 st i j k 2 nd i j k
162 161 a1i i 2 X n k X vol l X 1 st i n l k l X 2 nd i n l k = j k X vol 1 st i j k 2 nd i j k
163 78 eqcomd i 2 X j k X 1 st i j k 2 nd i j k = . i j k
164 163 fveq2d i 2 X j k X vol 1 st i j k 2 nd i j k = vol . i j k
165 164 prodeq2dv i 2 X j k X vol 1 st i j k 2 nd i j k = k X vol . i j k
166 165 mpteq2dva i 2 X j k X vol 1 st i j k 2 nd i j k = j k X vol . i j k
167 162 166 eqtrd i 2 X n k X vol l X 1 st i n l k l X 2 nd i n l k = j k X vol . i j k
168 167 fveq2d i 2 X sum^ n k X vol l X 1 st i n l k l X 2 nd i n l k = sum^ j k X vol . i j k
169 168 3ad2ant2 φ i 2 X z = sum^ j k X vol . i j k sum^ n k X vol l X 1 st i n l k l X 2 nd i n l k = sum^ j k X vol . i j k
170 92 adantll φ i 2 X n F i n = l X 1 st i n l
171 112 adantll φ i 2 X n S i n = l X 2 nd i n l
172 170 171 oveq12d φ i 2 X n F i n L X S i n = l X 1 st i n l L X l X 2 nd i n l
173 1 ad2antrr φ i 2 X n X Fin
174 2 ad2antrr φ i 2 X n X
175 23 adantlll φ i 2 X n l X i n l 2
176 175 24 syl φ i 2 X n l X 1 st i n l
177 176 fmpttd φ i 2 X n l X 1 st i n l : X
178 175 49 syl φ i 2 X n l X 2 nd i n l
179 178 fmpttd φ i 2 X n l X 2 nd i n l : X
180 6 173 174 177 179 hoidmvn0val φ i 2 X n l X 1 st i n l L X l X 2 nd i n l = k X vol l X 1 st i n l k l X 2 nd i n l k
181 172 180 eqtrd φ i 2 X n F i n L X S i n = k X vol l X 1 st i n l k l X 2 nd i n l k
182 181 mpteq2dva φ i 2 X n F i n L X S i n = n k X vol l X 1 st i n l k l X 2 nd i n l k
183 182 fveq2d φ i 2 X sum^ n F i n L X S i n = sum^ n k X vol l X 1 st i n l k l X 2 nd i n l k
184 183 3adant3 φ i 2 X z = sum^ j k X vol . i j k sum^ n F i n L X S i n = sum^ n k X vol l X 1 st i n l k l X 2 nd i n l k
185 simp3 φ i 2 X z = sum^ j k X vol . i j k z = sum^ j k X vol . i j k
186 169 184 185 3eqtr4d φ i 2 X z = sum^ j k X vol . i j k sum^ n F i n L X S i n = z
187 186 3adant3l φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k sum^ n F i n L X S i n = z
188 131 187 breqtrd φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k A L X B z
189 188 3exp φ i 2 X I j k X . i j k z = sum^ j k X vol . i j k A L X B z
190 189 adantr φ z M i 2 X I j k X . i j k z = sum^ j k X vol . i j k A L X B z
191 190 rexlimdv φ z M i 2 X I j k X . i j k z = sum^ j k X vol . i j k A L X B z
192 15 191 mpd φ z M A L X B z
193 192 ralrimiva φ z M A L X B z
194 ssrab2 z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k *
195 7 194 eqsstri M *
196 195 a1i φ M *
197 icossxr 0 +∞ *
198 6 1 3 4 hoidmvcl φ A L X B 0 +∞
199 197 198 sseldi φ A L X B *
200 infxrgelb M * A L X B * A L X B sup M * < z M A L X B z
201 196 199 200 syl2anc φ A L X B sup M * < z M A L X B z
202 193 201 mpbird φ A L X B sup M * <
203 5 a1i φ I = k X A k B k
204 nfv k φ
205 3 ffvelrnda φ k X A k
206 4 ffvelrnda φ k X B k
207 206 rexrd φ k X B k *
208 204 205 207 hoissrrn2 φ k X A k B k X
209 203 208 eqsstrd φ I X
210 1 2 209 7 ovnn0val φ voln* X I = sup M * <
211 210 eqcomd φ sup M * < = voln* X I
212 202 211 breqtrd φ A L X B voln* X I