Metamath Proof Explorer


Theorem hspmbllem2

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (b) of Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbllem2.h H = x Fin l x , y k x if k = l −∞ y
hspmbllem2.x φ X Fin
hspmbllem2.k φ K X
hspmbllem2.y φ Y
hspmbllem2.e φ E +
hspmbllem2.c φ C : X
hspmbllem2.d φ D : X
hspmbllem2.a φ A j k X C j k D j k
hspmbllem2.g φ sum^ j k X vol C j k D j k voln* X A + E
hspmbllem2.r φ voln* X A
hspmbllem2.i φ voln* X A K H X Y
hspmbllem2.f φ voln* X A K H X Y
hspmbllem2.l L = x Fin a x , b x if x = 0 k x vol a k b k
hspmbllem2.t T = y c X h X if h X K c h if c h y c h y
hspmbllem2.s S = x c X h X if h = K if x c h c h x c h
Assertion hspmbllem2 φ voln* X A K H X Y + voln* X A K H X Y voln* X A + E

Proof

Step Hyp Ref Expression
1 hspmbllem2.h H = x Fin l x , y k x if k = l −∞ y
2 hspmbllem2.x φ X Fin
3 hspmbllem2.k φ K X
4 hspmbllem2.y φ Y
5 hspmbllem2.e φ E +
6 hspmbllem2.c φ C : X
7 hspmbllem2.d φ D : X
8 hspmbllem2.a φ A j k X C j k D j k
9 hspmbllem2.g φ sum^ j k X vol C j k D j k voln* X A + E
10 hspmbllem2.r φ voln* X A
11 hspmbllem2.i φ voln* X A K H X Y
12 hspmbllem2.f φ voln* X A K H X Y
13 hspmbllem2.l L = x Fin a x , b x if x = 0 k x vol a k b k
14 hspmbllem2.t T = y c X h X if h X K c h if c h y c h y
15 hspmbllem2.s S = x c X h X if h = K if x c h c h x c h
16 11 12 readdcld φ voln* X A K H X Y + voln* X A K H X Y
17 5 rpred φ E
18 10 17 readdcld φ voln* X A + E
19 nfv j φ
20 nnex V
21 20 a1i φ V
22 icossicc 0 +∞ 0 +∞
23 2 adantr φ j X Fin
24 6 ffvelrnda φ j C j X
25 elmapi C j X C j : X
26 24 25 syl φ j C j : X
27 7 ffvelrnda φ j D j X
28 elmapi D j X D j : X
29 27 28 syl φ j D j : X
30 13 23 26 29 hoidmvcl φ j C j L X D j 0 +∞
31 22 30 sseldi φ j C j L X D j 0 +∞
32 19 21 31 sge0clmpt φ sum^ j C j L X D j 0 +∞
33 ne0i K X X
34 3 33 syl φ X
35 34 adantr φ j X
36 13 23 35 26 29 hoidmvn0val φ j C j L X D j = k X vol C j k D j k
37 36 mpteq2dva φ j C j L X D j = j k X vol C j k D j k
38 37 fveq2d φ sum^ j C j L X D j = sum^ j k X vol C j k D j k
39 38 9 eqbrtrd φ sum^ j C j L X D j voln* X A + E
40 18 32 39 ge0lere φ sum^ j C j L X D j
41 4 adantr φ j Y
42 14 41 23 29 hsphoif φ j T Y D j : X
43 13 23 26 42 hoidmvcl φ j C j L X T Y D j 0 +∞
44 22 43 sseldi φ j C j L X T Y D j 0 +∞
45 19 21 44 sge0clmpt φ sum^ j C j L X T Y D j 0 +∞
46 oveq2 x = y x = y
47 eqeq1 x = y x = y =
48 prodeq1 x = y k x vol a k b k = k y vol a k b k
49 47 48 ifbieq2d x = y if x = 0 k x vol a k b k = if y = 0 k y vol a k b k
50 46 46 49 mpoeq123dv x = y a x , b x if x = 0 k x vol a k b k = a y , b y if y = 0 k y vol a k b k
51 50 cbvmptv x Fin a x , b x if x = 0 k x vol a k b k = y Fin a y , b y if y = 0 k y vol a k b k
52 13 51 eqtri L = y Fin a y , b y if y = 0 k y vol a k b k
53 diffi X Fin X K Fin
54 2 53 syl φ X K Fin
55 snfi K Fin
56 55 a1i φ K Fin
57 unfi X K Fin K Fin X K K Fin
58 54 56 57 syl2anc φ X K K Fin
59 58 adantr φ j X K K Fin
60 snidg K X K K
61 3 60 syl φ K K
62 elun2 K K K X K K
63 61 62 syl φ K X K K
64 neldifsnd φ ¬ K X K
65 63 64 eldifd φ K X K K X K
66 65 adantr φ j K X K K X K
67 eqid X K K = X K K
68 eqid y c X K K h X K K if h X K c h if c h y c h y = y c X K K h X K K if h X K c h if c h y c h y
69 uncom X K K = K X K
70 69 a1i φ X K K = K X K
71 3 snssd φ K X
72 undif K X K X K = X
73 71 72 sylib φ K X K = X
74 70 73 eqtrd φ X K K = X
75 74 adantr φ j X K K = X
76 75 feq2d φ j C j : X K K C j : X
77 26 76 mpbird φ j C j : X K K
78 75 feq2d φ j D j : X K K D j : X
79 29 78 mpbird φ j D j : X K K
80 52 59 66 67 41 68 77 79 hsphoidmvle φ j C j L X K K y c X K K h X K K if h X K c h if c h y c h y Y D j C j L X K K D j
81 74 fveq2d φ L X K K = L X
82 eqidd φ C j = C j
83 14 a1i φ T = y c X h X if h X K c h if c h y c h y
84 74 oveq2d φ X K K = X
85 74 mpteq1d φ h X K K if h X K c h if c h y c h y = h X if h X K c h if c h y c h y
86 84 85 mpteq12dv φ c X K K h X K K if h X K c h if c h y c h y = c X h X if h X K c h if c h y c h y
87 86 eqcomd φ c X h X if h X K c h if c h y c h y = c X K K h X K K if h X K c h if c h y c h y
88 87 mpteq2dv φ y c X h X if h X K c h if c h y c h y = y c X K K h X K K if h X K c h if c h y c h y
89 83 88 eqtr2d φ y c X K K h X K K if h X K c h if c h y c h y = T
90 89 fveq1d φ y c X K K h X K K if h X K c h if c h y c h y Y = T Y
91 90 fveq1d φ y c X K K h X K K if h X K c h if c h y c h y Y D j = T Y D j
92 81 82 91 oveq123d φ C j L X K K y c X K K h X K K if h X K c h if c h y c h y Y D j = C j L X T Y D j
93 92 adantr φ j C j L X K K y c X K K h X K K if h X K c h if c h y c h y Y D j = C j L X T Y D j
94 81 adantr φ j L X K K = L X
95 94 oveqd φ j C j L X K K D j = C j L X D j
96 93 95 breq12d φ j C j L X K K y c X K K h X K K if h X K c h if c h y c h y Y D j C j L X K K D j C j L X T Y D j C j L X D j
97 80 96 mpbid φ j C j L X T Y D j C j L X D j
98 19 21 44 31 97 sge0lempt φ sum^ j C j L X T Y D j sum^ j C j L X D j
99 40 45 98 ge0lere φ sum^ j C j L X T Y D j
100 15 41 23 26 hoidifhspf φ j S Y C j : X
101 13 23 100 29 hoidmvcl φ j S Y C j L X D j 0 +∞
102 101 fmpttd φ j S Y C j L X D j : 0 +∞
103 22 a1i φ 0 +∞ 0 +∞
104 102 103 fssd φ j S Y C j L X D j : 0 +∞
105 21 104 sge0cl φ sum^ j S Y C j L X D j 0 +∞
106 22 101 sseldi φ j S Y C j L X D j 0 +∞
107 3 adantr φ j K X
108 13 23 26 29 107 15 41 hoidifhspdmvle φ j S Y C j L X D j C j L X D j
109 19 21 106 31 108 sge0lempt φ sum^ j S Y C j L X D j sum^ j C j L X D j
110 40 105 109 ge0lere φ sum^ j S Y C j L X D j
111 4 adantr φ l Y
112 2 adantr φ l X Fin
113 eleq1w j = l j l
114 113 anbi2d j = l φ j φ l
115 fveq2 j = l D j = D l
116 115 feq1d j = l D j : X D l : X
117 114 116 imbi12d j = l φ j D j : X φ l D l : X
118 117 29 chvarvv φ l D l : X
119 14 111 112 118 hsphoif φ l T Y D l : X
120 reex V
121 120 a1i φ V
122 121 2 jca φ V X Fin
123 122 adantr φ l V X Fin
124 elmapg V X Fin T Y D l X T Y D l : X
125 123 124 syl φ l T Y D l X T Y D l : X
126 119 125 mpbird φ l T Y D l X
127 126 fmpttd φ l T Y D l : X
128 simpl φ f A K H X Y φ
129 elinel1 f A K H X Y f A
130 129 adantl φ f A K H X Y f A
131 8 sselda φ f A f j k X C j k D j k
132 eliun f j k X C j k D j k j f k X C j k D j k
133 131 132 sylib φ f A j f k X C j k D j k
134 128 130 133 syl2anc φ f A K H X Y j f k X C j k D j k
135 simpll φ f A K H X Y j φ
136 elinel2 f A K H X Y f K H X Y
137 136 adantl φ f A K H X Y f K H X Y
138 137 adantr φ f A K H X Y j f K H X Y
139 simpr φ f A K H X Y j j
140 ixpfn f k X C j k D j k f Fn X
141 140 adantl φ f K H X Y j f k X C j k D j k f Fn X
142 nfv k φ f K H X Y j
143 nfcv _ k f
144 nfixp1 _ k k X C j k D j k
145 143 144 nfel k f k X C j k D j k
146 142 145 nfan k φ f K H X Y j f k X C j k D j k
147 26 3adant3 φ j k X C j : X
148 simp3 φ j k X k X
149 147 148 ffvelrnd φ j k X C j k
150 149 rexrd φ j k X C j k *
151 150 ad5ant135 φ f K H X Y j f k X C j k D j k k X C j k *
152 42 3adant3 φ j k X T Y D j : X
153 152 148 ffvelrnd φ j k X T Y D j k
154 153 rexrd φ j k X T Y D j k *
155 154 ad5ant135 φ f K H X Y j f k X C j k D j k k X T Y D j k *
156 iftrue k = K if k = K −∞ Y = −∞ Y
157 ioossre −∞ Y
158 157 a1i k = K −∞ Y
159 156 158 eqsstrd k = K if k = K −∞ Y
160 iffalse ¬ k = K if k = K −∞ Y =
161 ssid
162 161 a1i ¬ k = K
163 160 162 eqsstrd ¬ k = K if k = K −∞ Y
164 159 163 pm2.61i if k = K −∞ Y
165 simpr φ f K H X Y f K H X Y
166 1 2 3 4 hspval φ K H X Y = k X if k = K −∞ Y
167 166 adantr φ f K H X Y K H X Y = k X if k = K −∞ Y
168 165 167 eleqtrd φ f K H X Y f k X if k = K −∞ Y
169 168 adantr φ f K H X Y k X f k X if k = K −∞ Y
170 simpr φ f K H X Y k X k X
171 vex f V
172 171 elixp f k X if k = K −∞ Y f Fn X k X f k if k = K −∞ Y
173 172 biimpi f k X if k = K −∞ Y f Fn X k X f k if k = K −∞ Y
174 173 simprd f k X if k = K −∞ Y k X f k if k = K −∞ Y
175 174 adantr f k X if k = K −∞ Y k X k X f k if k = K −∞ Y
176 simpr f k X if k = K −∞ Y k X k X
177 rspa k X f k if k = K −∞ Y k X f k if k = K −∞ Y
178 175 176 177 syl2anc f k X if k = K −∞ Y k X f k if k = K −∞ Y
179 169 170 178 syl2anc φ f K H X Y k X f k if k = K −∞ Y
180 164 179 sseldi φ f K H X Y k X f k
181 180 rexrd φ f K H X Y k X f k *
182 181 ad4ant14 φ f K H X Y j f k X C j k D j k k X f k *
183 150 ad4ant124 φ j f k X C j k D j k k X C j k *
184 29 3adant3 φ j k X D j : X
185 184 148 ffvelrnd φ j k X D j k
186 185 rexrd φ j k X D j k *
187 186 ad4ant124 φ j f k X C j k D j k k X D j k *
188 171 elixp f k X C j k D j k f Fn X k X f k C j k D j k
189 188 biimpi f k X C j k D j k f Fn X k X f k C j k D j k
190 189 simprd f k X C j k D j k k X f k C j k D j k
191 190 adantr f k X C j k D j k k X k X f k C j k D j k
192 simpr f k X C j k D j k k X k X
193 rspa k X f k C j k D j k k X f k C j k D j k
194 191 192 193 syl2anc f k X C j k D j k k X f k C j k D j k
195 194 adantll φ j f k X C j k D j k k X f k C j k D j k
196 icogelb C j k * D j k * f k C j k D j k C j k f k
197 183 187 195 196 syl3anc φ j f k X C j k D j k k X C j k f k
198 197 adantl3r φ f K H X Y j f k X C j k D j k k X C j k f k
199 icoltub C j k * D j k * f k C j k D j k f k < D j k
200 183 187 195 199 syl3anc φ j f k X C j k D j k k X f k < D j k
201 200 adantl3r φ f K H X Y j f k X C j k D j k k X f k < D j k
202 201 ad2antrr φ f K H X Y j f k X C j k D j k k X k = K D j k Y f k < D j k
203 simpll φ f K H X Y j φ
204 simpr φ f K H X Y j j
205 203 204 jca φ f K H X Y j φ j
206 205 3ad2ant1 φ f K H X Y j k = K D j k Y φ j
207 simp2 φ f K H X Y j k = K D j k Y k = K
208 simp3 φ f K H X Y j k = K D j k Y D j k Y
209 fveq2 k = K D j k = D j K
210 209 breq1d k = K D j k Y D j K Y
211 210 biimpa k = K D j k Y D j K Y
212 211 iftrued k = K D j k Y if D j K Y D j K Y = D j K
213 209 eqcomd k = K D j K = D j k
214 213 adantr k = K D j k Y D j K = D j k
215 212 214 eqtrd k = K D j k Y if D j K Y D j K Y = D j k
216 215 3adant1 φ j k = K D j k Y if D j K Y D j K Y = D j k
217 breq2 y = Y c h y c h Y
218 id y = Y y = Y
219 217 218 ifbieq2d y = Y if c h y c h y = if c h Y c h Y
220 219 ifeq2d y = Y if h X K c h if c h y c h y = if h X K c h if c h Y c h Y
221 220 mpteq2dv y = Y h X if h X K c h if c h y c h y = h X if h X K c h if c h Y c h Y
222 221 mpteq2dv y = Y c X h X if h X K c h if c h y c h y = c X h X if h X K c h if c h Y c h Y
223 ovex X V
224 223 mptex c X h X if h X K c h if c h Y c h Y V
225 224 a1i φ c X h X if h X K c h if c h Y c h Y V
226 14 222 4 225 fvmptd3 φ T Y = c X h X if h X K c h if c h Y c h Y
227 226 adantr φ j T Y = c X h X if h X K c h if c h Y c h Y
228 fveq1 c = D j c h = D j h
229 228 breq1d c = D j c h Y D j h Y
230 229 228 ifbieq1d c = D j if c h Y c h Y = if D j h Y D j h Y
231 228 230 ifeq12d c = D j if h X K c h if c h Y c h Y = if h X K D j h if D j h Y D j h Y
232 231 mpteq2dv c = D j h X if h X K c h if c h Y c h Y = h X if h X K D j h if D j h Y D j h Y
233 232 adantl φ j c = D j h X if h X K c h if c h Y c h Y = h X if h X K D j h if D j h Y D j h Y
234 mptexg X Fin h X if h X K D j h if D j h Y D j h Y V
235 2 234 syl φ h X if h X K D j h if D j h Y D j h Y V
236 235 adantr φ j h X if h X K D j h if D j h Y D j h Y V
237 227 233 27 236 fvmptd φ j T Y D j = h X if h X K D j h if D j h Y D j h Y
238 237 fveq1d φ j T Y D j k = h X if h X K D j h if D j h Y D j h Y k
239 238 3adant3 φ j k = K T Y D j k = h X if h X K D j h if D j h Y D j h Y k
240 simpl φ k = K φ
241 simpr φ k = K k = K
242 240 3 syl φ k = K K X
243 241 242 eqeltrd φ k = K k X
244 eqidd φ k X h X if h X K D j h if D j h Y D j h Y = h X if h X K D j h if D j h Y D j h Y
245 eleq1w h = k h X K k X K
246 fveq2 h = k D j h = D j k
247 246 breq1d h = k D j h Y D j k Y
248 247 246 ifbieq1d h = k if D j h Y D j h Y = if D j k Y D j k Y
249 245 246 248 ifbieq12d h = k if h X K D j h if D j h Y D j h Y = if k X K D j k if D j k Y D j k Y
250 249 adantl φ k X h = k if h X K D j h if D j h Y D j h Y = if k X K D j k if D j k Y D j k Y
251 simpr φ k X k X
252 fvexd φ D j k V
253 252 4 ifexd φ if D j k Y D j k Y V
254 252 253 ifexd φ if k X K D j k if D j k Y D j k Y V
255 254 adantr φ k X if k X K D j k if D j k Y D j k Y V
256 244 250 251 255 fvmptd φ k X h X if h X K D j h if D j h Y D j h Y k = if k X K D j k if D j k Y D j k Y
257 240 243 256 syl2anc φ k = K h X if h X K D j h if D j h Y D j h Y k = if k X K D j k if D j k Y D j k Y
258 eleq1 k = K k X K K X K
259 210 209 ifbieq1d k = K if D j k Y D j k Y = if D j K Y D j K Y
260 258 209 259 ifbieq12d k = K if k X K D j k if D j k Y D j k Y = if K X K D j K if D j K Y D j K Y
261 260 adantl φ k = K if k X K D j k if D j k Y D j k Y = if K X K D j K if D j K Y D j K Y
262 257 261 eqtrd φ k = K h X if h X K D j h if D j h Y D j h Y k = if K X K D j K if D j K Y D j K Y
263 262 3adant2 φ j k = K h X if h X K D j h if D j h Y D j h Y k = if K X K D j K if D j K Y D j K Y
264 neldifsnd k = K ¬ K X K
265 264 iffalsed k = K if K X K D j K if D j K Y D j K Y = if D j K Y D j K Y
266 265 3ad2ant3 φ j k = K if K X K D j K if D j K Y D j K Y = if D j K Y D j K Y
267 239 263 266 3eqtrrd φ j k = K if D j K Y D j K Y = T Y D j k
268 267 3expa φ j k = K if D j K Y D j K Y = T Y D j k
269 268 3adant3 φ j k = K D j k Y if D j K Y D j K Y = T Y D j k
270 216 269 eqtr3d φ j k = K D j k Y D j k = T Y D j k
271 206 207 208 270 syl3anc φ f K H X Y j k = K D j k Y D j k = T Y D j k
272 271 ad5ant145 φ f K H X Y j f k X C j k D j k k X k = K D j k Y D j k = T Y D j k
273 202 272 breqtrd φ f K H X Y j f k X C j k D j k k X k = K D j k Y f k < T Y D j k
274 mnfxr −∞ *
275 274 a1i φ f K H X Y k X k = K −∞ *
276 4 rexrd φ Y *
277 276 adantr φ f K H X Y Y *
278 277 3ad2ant1 φ f K H X Y k X k = K Y *
279 179 3adant3 φ f K H X Y k X k = K f k if k = K −∞ Y
280 156 3ad2ant3 φ f K H X Y k X k = K if k = K −∞ Y = −∞ Y
281 279 280 eleqtrd φ f K H X Y k X k = K f k −∞ Y
282 iooltub −∞ * Y * f k −∞ Y f k < Y
283 275 278 281 282 syl3anc φ f K H X Y k X k = K f k < Y
284 283 3adant1r φ f K H X Y j k X k = K f k < Y
285 284 ad4ant123 φ f K H X Y j k X k = K ¬ D j k Y f k < Y
286 simpr k = K ¬ D j k Y ¬ D j k Y
287 210 notbid k = K ¬ D j k Y ¬ D j K Y
288 287 adantr k = K ¬ D j k Y ¬ D j k Y ¬ D j K Y
289 286 288 mpbid k = K ¬ D j k Y ¬ D j K Y
290 289 iffalsed k = K ¬ D j k Y if D j K Y D j K Y = Y
291 eqidd k = K ¬ D j k Y Y = Y
292 290 291 eqtr2d k = K ¬ D j k Y Y = if D j K Y D j K Y
293 292 adantll φ f K H X Y j k X k = K ¬ D j k Y Y = if D j K Y D j K Y
294 268 adantlr φ j k X k = K if D j K Y D j K Y = T Y D j k
295 294 adantl3r φ f K H X Y j k X k = K if D j K Y D j K Y = T Y D j k
296 295 adantr φ f K H X Y j k X k = K ¬ D j k Y if D j K Y D j K Y = T Y D j k
297 293 296 eqtrd φ f K H X Y j k X k = K ¬ D j k Y Y = T Y D j k
298 285 297 breqtrd φ f K H X Y j k X k = K ¬ D j k Y f k < T Y D j k
299 298 adantl3r φ f K H X Y j f k X C j k D j k k X k = K ¬ D j k Y f k < T Y D j k
300 273 299 pm2.61dan φ f K H X Y j f k X C j k D j k k X k = K f k < T Y D j k
301 201 adantr φ f K H X Y j f k X C j k D j k k X ¬ k = K f k < D j k
302 237 3adant3 φ j k X T Y D j = h X if h X K D j h if D j h Y D j h Y
303 249 adantl φ j k X h = k if h X K D j h if D j h Y D j h Y = if k X K D j k if D j k Y D j k Y
304 255 3adant2 φ j k X if k X K D j k if D j k Y D j k Y V
305 302 303 148 304 fvmptd φ j k X T Y D j k = if k X K D j k if D j k Y D j k Y
306 305 3expa φ j k X T Y D j k = if k X K D j k if D j k Y D j k Y
307 306 adantllr φ f K H X Y j k X T Y D j k = if k X K D j k if D j k Y D j k Y
308 307 ad4ant13 φ f K H X Y j f k X C j k D j k k X ¬ k = K T Y D j k = if k X K D j k if D j k Y D j k Y
309 simpl k X ¬ k = K k X
310 neqne ¬ k = K k K
311 nelsn k K ¬ k K
312 310 311 syl ¬ k = K ¬ k K
313 312 adantl k X ¬ k = K ¬ k K
314 309 313 eldifd k X ¬ k = K k X K
315 314 iftrued k X ¬ k = K if k X K D j k if D j k Y D j k Y = D j k
316 315 adantll φ f K H X Y j f k X C j k D j k k X ¬ k = K if k X K D j k if D j k Y D j k Y = D j k
317 308 316 eqtr2d φ f K H X Y j f k X C j k D j k k X ¬ k = K D j k = T Y D j k
318 301 317 breqtrd φ f K H X Y j f k X C j k D j k k X ¬ k = K f k < T Y D j k
319 300 318 pm2.61dan φ f K H X Y j f k X C j k D j k k X f k < T Y D j k
320 151 155 182 198 319 elicod φ f K H X Y j f k X C j k D j k k X f k C j k T Y D j k
321 320 ex φ f K H X Y j f k X C j k D j k k X f k C j k T Y D j k
322 146 321 ralrimi φ f K H X Y j f k X C j k D j k k X f k C j k T Y D j k
323 141 322 jca φ f K H X Y j f k X C j k D j k f Fn X k X f k C j k T Y D j k
324 171 elixp f k X C j k T Y D j k f Fn X k X f k C j k T Y D j k
325 323 324 sylibr φ f K H X Y j f k X C j k D j k f k X C j k T Y D j k
326 325 ex φ f K H X Y j f k X C j k D j k f k X C j k T Y D j k
327 135 138 139 326 syl21anc φ f A K H X Y j f k X C j k D j k f k X C j k T Y D j k
328 327 reximdva φ f A K H X Y j f k X C j k D j k j f k X C j k T Y D j k
329 134 328 mpd φ f A K H X Y j f k X C j k T Y D j k
330 eliun f j k X C j k T Y D j k j f k X C j k T Y D j k
331 329 330 sylibr φ f A K H X Y f j k X C j k T Y D j k
332 331 ralrimiva φ f A K H X Y f j k X C j k T Y D j k
333 dfss3 A K H X Y j k X C j k T Y D j k f A K H X Y f j k X C j k T Y D j k
334 332 333 sylibr φ A K H X Y j k X C j k T Y D j k
335 eqidd j l T Y D l = l T Y D l
336 2fveq3 l = j T Y D l = T Y D j
337 336 adantl j l = j T Y D l = T Y D j
338 id j j
339 fvexd j T Y D j V
340 335 337 338 339 fvmptd j l T Y D l j = T Y D j
341 340 fveq1d j l T Y D l j k = T Y D j k
342 341 oveq2d j C j k l T Y D l j k = C j k T Y D j k
343 342 ixpeq2dv j k X C j k l T Y D l j k = k X C j k T Y D j k
344 343 iuneq2i j k X C j k l T Y D l j k = j k X C j k T Y D j k
345 334 344 sseqtrrdi φ A K H X Y j k X C j k l T Y D l j k
346 2 6 127 345 13 ovnlecvr2 φ voln* X A K H X Y sum^ j C j L X l T Y D l j
347 340 oveq2d j C j L X l T Y D l j = C j L X T Y D j
348 347 mpteq2ia j C j L X l T Y D l j = j C j L X T Y D j
349 348 fveq2i sum^ j C j L X l T Y D l j = sum^ j C j L X T Y D j
350 349 a1i φ sum^ j C j L X l T Y D l j = sum^ j C j L X T Y D j
351 346 350 breqtrd φ voln* X A K H X Y sum^ j C j L X T Y D j
352 6 ffvelrnda φ l C l X
353 elmapi C l X C l : X
354 352 353 syl φ l C l : X
355 15 111 112 354 hoidifhspf φ l S Y C l : X
356 elmapg V X Fin S Y C l X S Y C l : X
357 122 356 syl φ S Y C l X S Y C l : X
358 357 adantr φ l S Y C l X S Y C l : X
359 355 358 mpbird φ l S Y C l X
360 359 fmpttd φ l S Y C l : X
361 simpl φ f A K H X Y φ
362 eldifi f A K H X Y f A
363 362 adantl φ f A K H X Y f A
364 361 363 133 syl2anc φ f A K H X Y j f k X C j k D j k
365 140 adantl φ f A K H X Y j f k X C j k D j k f Fn X
366 nfv k φ f A K H X Y j
367 366 145 nfan k φ f A K H X Y j f k X C j k D j k
368 100 3adant3 φ j k X S Y C j : X
369 368 148 ffvelrnd φ j k X S Y C j k
370 369 rexrd φ j k X S Y C j k *
371 370 ad5ant135 φ f A K H X Y j f k X C j k D j k k X S Y C j k *
372 187 adantl3r φ f A K H X Y j f k X C j k D j k k X D j k *
373 149 3expa φ j k X C j k
374 186 3expa φ j k X D j k *
375 icossre C j k D j k * C j k D j k
376 373 374 375 syl2anc φ j k X C j k D j k
377 376 adantlr φ j f k X C j k D j k k X C j k D j k
378 377 195 sseldd φ j f k X C j k D j k k X f k
379 378 rexrd φ j f k X C j k D j k k X f k *
380 379 adantl3r φ f A K H X Y j f k X C j k D j k k X f k *
381 41 3adant3 φ j k X Y
382 23 3adant3 φ j k X X Fin
383 15 381 382 147 148 hoidifhspval3 φ j k X S Y C j k = if k = K if Y C j k C j k Y C j k
384 383 ad5ant134 φ f A K H X Y j k X k = K S Y C j k = if k = K if Y C j k C j k Y C j k
385 iftrue k = K if k = K if Y C j k C j k Y C j k = if Y C j k C j k Y
386 385 adantl φ f A K H X Y j k X k = K if k = K if Y C j k C j k Y C j k = if Y C j k C j k Y
387 384 386 eqtrd φ f A K H X Y j k X k = K S Y C j k = if Y C j k C j k Y
388 387 adantllr φ f A K H X Y j f k X C j k D j k k X k = K S Y C j k = if Y C j k C j k Y
389 iftrue Y C j k if Y C j k C j k Y = C j k
390 389 adantl φ f A K H X Y j f k X C j k D j k k X k = K Y C j k if Y C j k C j k Y = C j k
391 197 adantl3r φ f A K H X Y j f k X C j k D j k k X C j k f k
392 391 ad2antrr φ f A K H X Y j f k X C j k D j k k X k = K Y C j k C j k f k
393 390 392 eqbrtrd φ f A K H X Y j f k X C j k D j k k X k = K Y C j k if Y C j k C j k Y f k
394 iffalse ¬ Y C j k if Y C j k C j k Y = Y
395 394 adantl φ f A K H X Y j f k X C j k D j k k X k = K ¬ Y C j k if Y C j k C j k Y = Y
396 simpl1 φ f A K H X Y k X k = K ¬ Y f k φ f A K H X Y
397 simpr k = K ¬ Y f k ¬ Y f k
398 fveq2 k = K f k = f K
399 398 breq2d k = K Y f k Y f K
400 399 notbid k = K ¬ Y f k ¬ Y f K
401 400 adantr k = K ¬ Y f k ¬ Y f k ¬ Y f K
402 397 401 mpbid k = K ¬ Y f k ¬ Y f K
403 402 3ad2antl3 φ f A K H X Y k X k = K ¬ Y f k ¬ Y f K
404 398 eqcomd k = K f K = f k
405 404 3ad2ant3 φ f A K H X Y k X k = K f K = f k
406 364 adantr φ f A K H X Y k X j f k X C j k D j k
407 id φ j φ j
408 407 ad4ant13 φ k X j f k X C j k D j k φ j
409 simpr φ k X j f k X C j k D j k f k X C j k D j k
410 251 ad2antrr φ k X j f k X C j k D j k k X
411 408 409 410 378 syl21anc φ k X j f k X C j k D j k f k
412 411 rexlimdva2 φ k X j f k X C j k D j k f k
413 412 adantlr φ f A K H X Y k X j f k X C j k D j k f k
414 406 413 mpd φ f A K H X Y k X f k
415 414 3adant3 φ f A K H X Y k X k = K f k
416 405 415 eqeltrd φ f A K H X Y k X k = K f K
417 416 adantr φ f A K H X Y k X k = K ¬ Y f k f K
418 396 361 4 3syl φ f A K H X Y k X k = K ¬ Y f k Y
419 417 418 ltnled φ f A K H X Y k X k = K ¬ Y f k f K < Y ¬ Y f K
420 403 419 mpbird φ f A K H X Y k X k = K ¬ Y f k f K < Y
421 365 364 r19.29a φ f A K H X Y f Fn X
422 421 adantr φ f A K H X Y f K < Y f Fn X
423 274 a1i φ f A K H X Y f K < Y k X k = K −∞ *
424 276 ad4antr φ f A K H X Y f K < Y k X k = K Y *
425 414 ad4ant13 φ f A K H X Y f K < Y k X k = K f k
426 425 mnfltd φ f A K H X Y f K < Y k X k = K −∞ < f k
427 398 adantl f K < Y k = K f k = f K
428 simpl f K < Y k = K f K < Y
429 427 428 eqbrtrd f K < Y k = K f k < Y
430 429 ad4ant24 φ f A K H X Y f K < Y k X k = K f k < Y
431 423 424 425 426 430 eliood φ f A K H X Y f K < Y k X k = K f k −∞ Y
432 156 eqcomd k = K −∞ Y = if k = K −∞ Y
433 432 adantl φ f A K H X Y f K < Y k X k = K −∞ Y = if k = K −∞ Y
434 431 433 eleqtrd φ f A K H X Y f K < Y k X k = K f k if k = K −∞ Y
435 414 ad4ant13 φ f A K H X Y f K < Y k X ¬ k = K f k
436 160 eqcomd ¬ k = K = if k = K −∞ Y
437 436 adantl φ f A K H X Y f K < Y k X ¬ k = K = if k = K −∞ Y
438 435 437 eleqtrd φ f A K H X Y f K < Y k X ¬ k = K f k if k = K −∞ Y
439 434 438 pm2.61dan φ f A K H X Y f K < Y k X f k if k = K −∞ Y
440 439 ralrimiva φ f A K H X Y f K < Y k X f k if k = K −∞ Y
441 422 440 jca φ f A K H X Y f K < Y f Fn X k X f k if k = K −∞ Y
442 396 420 441 syl2anc φ f A K H X Y k X k = K ¬ Y f k f Fn X k X f k if k = K −∞ Y
443 442 172 sylibr φ f A K H X Y k X k = K ¬ Y f k f k X if k = K −∞ Y
444 166 eqcomd φ k X if k = K −∞ Y = K H X Y
445 444 ad2antrr φ f A K H X Y ¬ Y f k k X if k = K −∞ Y = K H X Y
446 445 3ad2antl1 φ f A K H X Y k X k = K ¬ Y f k k X if k = K −∞ Y = K H X Y
447 443 446 eleqtrd φ f A K H X Y k X k = K ¬ Y f k f K H X Y
448 eldifn f A K H X Y ¬ f K H X Y
449 448 adantl φ f A K H X Y ¬ f K H X Y
450 449 3ad2ant1 φ f A K H X Y k X k = K ¬ f K H X Y
451 450 adantr φ f A K H X Y k X k = K ¬ Y f k ¬ f K H X Y
452 447 451 condan φ f A K H X Y k X k = K Y f k
453 452 ad5ant145 φ f A K H X Y j f k X C j k D j k k X k = K Y f k
454 453 adantr φ f A K H X Y j f k X C j k D j k k X k = K ¬ Y C j k Y f k
455 395 454 eqbrtrd φ f A K H X Y j f k X C j k D j k k X k = K ¬ Y C j k if Y C j k C j k Y f k
456 393 455 pm2.61dan φ f A K H X Y j f k X C j k D j k k X k = K if Y C j k C j k Y f k
457 388 456 eqbrtrd φ f A K H X Y j f k X C j k D j k k X k = K S Y C j k f k
458 383 ad5ant124 φ j f k X C j k D j k k X ¬ k = K S Y C j k = if k = K if Y C j k C j k Y C j k
459 iffalse ¬ k = K if k = K if Y C j k C j k Y C j k = C j k
460 459 adantl φ j f k X C j k D j k k X ¬ k = K if k = K if Y C j k C j k Y C j k = C j k
461 458 460 eqtrd φ j f k X C j k D j k k X ¬ k = K S Y C j k = C j k
462 197 adantr φ j f k X C j k D j k k X ¬ k = K C j k f k
463 461 462 eqbrtrd φ j f k X C j k D j k k X ¬ k = K S Y C j k f k
464 463 adantl4r φ f A K H X Y j f k X C j k D j k k X ¬ k = K S Y C j k f k
465 457 464 pm2.61dan φ f A K H X Y j f k X C j k D j k k X S Y C j k f k
466 200 adantl3r φ f A K H X Y j f k X C j k D j k k X f k < D j k
467 371 372 380 465 466 elicod φ f A K H X Y j f k X C j k D j k k X f k S Y C j k D j k
468 467 ex φ f A K H X Y j f k X C j k D j k k X f k S Y C j k D j k
469 367 468 ralrimi φ f A K H X Y j f k X C j k D j k k X f k S Y C j k D j k
470 365 469 jca φ f A K H X Y j f k X C j k D j k f Fn X k X f k S Y C j k D j k
471 171 elixp f k X S Y C j k D j k f Fn X k X f k S Y C j k D j k
472 470 471 sylibr φ f A K H X Y j f k X C j k D j k f k X S Y C j k D j k
473 eqidd j l S Y C l = l S Y C l
474 2fveq3 l = j S Y C l = S Y C j
475 474 adantl j l = j S Y C l = S Y C j
476 fvexd j S Y C j V
477 473 475 338 476 fvmptd j l S Y C l j = S Y C j
478 477 fveq1d j l S Y C l j k = S Y C j k
479 478 oveq1d j l S Y C l j k D j k = S Y C j k D j k
480 479 ixpeq2dv j k X l S Y C l j k D j k = k X S Y C j k D j k
481 480 ad2antlr φ f A K H X Y j f k X C j k D j k k X l S Y C l j k D j k = k X S Y C j k D j k
482 481 eleq2d φ f A K H X Y j f k X C j k D j k f k X l S Y C l j k D j k f k X S Y C j k D j k
483 472 482 mpbird φ f A K H X Y j f k X C j k D j k f k X l S Y C l j k D j k
484 483 ex φ f A K H X Y j f k X C j k D j k f k X l S Y C l j k D j k
485 484 reximdva φ f A K H X Y j f k X C j k D j k j f k X l S Y C l j k D j k
486 364 485 mpd φ f A K H X Y j f k X l S Y C l j k D j k
487 eliun f j k X l S Y C l j k D j k j f k X l S Y C l j k D j k
488 486 487 sylibr φ f A K H X Y f j k X l S Y C l j k D j k
489 488 ralrimiva φ f A K H X Y f j k X l S Y C l j k D j k
490 dfss3 A K H X Y j k X l S Y C l j k D j k f A K H X Y f j k X l S Y C l j k D j k
491 489 490 sylibr φ A K H X Y j k X l S Y C l j k D j k
492 2 360 7 491 13 ovnlecvr2 φ voln* X A K H X Y sum^ j l S Y C l j L X D j
493 477 oveq1d j l S Y C l j L X D j = S Y C j L X D j
494 493 mpteq2ia j l S Y C l j L X D j = j S Y C j L X D j
495 494 fveq2i sum^ j l S Y C l j L X D j = sum^ j S Y C j L X D j
496 495 a1i φ sum^ j l S Y C l j L X D j = sum^ j S Y C j L X D j
497 492 496 breqtrd φ voln* X A K H X Y sum^ j S Y C j L X D j
498 11 12 99 110 351 497 leadd12dd φ voln* X A K H X Y + voln* X A K H X Y sum^ j C j L X T Y D j + sum^ j S Y C j L X D j
499 23 107 41 26 29 13 14 15 hspmbllem1 φ j C j L X D j = C j L X T Y D j + 𝑒 S Y C j L X D j
500 499 mpteq2dva φ j C j L X D j = j C j L X T Y D j + 𝑒 S Y C j L X D j
501 500 fveq2d φ sum^ j C j L X D j = sum^ j C j L X T Y D j + 𝑒 S Y C j L X D j
502 19 21 44 106 sge0xadd φ sum^ j C j L X T Y D j + 𝑒 S Y C j L X D j = sum^ j C j L X T Y D j + 𝑒 sum^ j S Y C j L X D j
503 99 110 rexaddd φ sum^ j C j L X T Y D j + 𝑒 sum^ j S Y C j L X D j = sum^ j C j L X T Y D j + sum^ j S Y C j L X D j
504 501 502 503 3eqtrrd φ sum^ j C j L X T Y D j + sum^ j S Y C j L X D j = sum^ j C j L X D j
505 498 504 breqtrd φ voln* X A K H X Y + voln* X A K H X Y sum^ j C j L X D j
506 16 40 18 505 39 letrd φ voln* X A K H X Y + voln* X A K H X Y voln* X A + E