Metamath Proof Explorer


Theorem stoweidlem59

Description: This lemma proves that there exists a function x as in the proof in BrosowskiDeutsh p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - \epsilon / n on B_j. Here D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem59.1 _tF
stoweidlem59.2 tφ
stoweidlem59.3 K=topGenran.
stoweidlem59.4 T=J
stoweidlem59.5 C=JCnK
stoweidlem59.6 D=j0NtT|Ftj13E
stoweidlem59.7 B=j0NtT|j+13EFt
stoweidlem59.8 Y=yA|tT0ytyt1
stoweidlem59.9 H=j0NyY|tDjyt<ENtBj1EN<yt
stoweidlem59.10 φJComp
stoweidlem59.11 φAC
stoweidlem59.12 φfAgAtTft+gtA
stoweidlem59.13 φfAgAtTftgtA
stoweidlem59.14 φytTyA
stoweidlem59.15 φrTtTrtqAqrqt
stoweidlem59.16 φFC
stoweidlem59.17 φE+
stoweidlem59.18 φE<13
stoweidlem59.19 φN
Assertion stoweidlem59 φxx:0NAj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjt

Proof

Step Hyp Ref Expression
1 stoweidlem59.1 _tF
2 stoweidlem59.2 tφ
3 stoweidlem59.3 K=topGenran.
4 stoweidlem59.4 T=J
5 stoweidlem59.5 C=JCnK
6 stoweidlem59.6 D=j0NtT|Ftj13E
7 stoweidlem59.7 B=j0NtT|j+13EFt
8 stoweidlem59.8 Y=yA|tT0ytyt1
9 stoweidlem59.9 H=j0NyY|tDjyt<ENtBj1EN<yt
10 stoweidlem59.10 φJComp
11 stoweidlem59.11 φAC
12 stoweidlem59.12 φfAgAtTft+gtA
13 stoweidlem59.13 φfAgAtTftgtA
14 stoweidlem59.14 φytTyA
15 stoweidlem59.15 φrTtTrtqAqrqt
16 stoweidlem59.16 φFC
17 stoweidlem59.17 φE+
18 stoweidlem59.18 φE<13
19 stoweidlem59.19 φN
20 nfrab1 _yyA|tT0ytyt1
21 8 20 nfcxfr _yY
22 nfcv _zY
23 nfv ztDjyt<ENtBj1EN<yt
24 nfv ytDjzt<ENtBj1EN<zt
25 fveq1 y=zyt=zt
26 25 breq1d y=zyt<ENzt<EN
27 26 ralbidv y=ztDjyt<ENtDjzt<EN
28 25 breq2d y=z1EN<yt1EN<zt
29 28 ralbidv y=ztBj1EN<yttBj1EN<zt
30 27 29 anbi12d y=ztDjyt<ENtBj1EN<yttDjzt<ENtBj1EN<zt
31 21 22 23 24 30 cbvrabw yY|tDjyt<ENtBj1EN<yt=zY|tDjzt<ENtBj1EN<zt
32 ovexd φJCnKV
33 11 5 sseqtrdi φAJCnK
34 32 33 ssexd φAV
35 8 34 rabexd φYV
36 31 35 rabexd φyY|tDjyt<ENtBj1EN<ytV
37 36 ralrimivw φj0NyY|tDjyt<ENtBj1EN<ytV
38 9 fnmpt j0NyY|tDjyt<ENtBj1EN<ytVHFn0N
39 37 38 syl φHFn0N
40 fzfi 0NFin
41 fnfi HFn0N0NFinHFin
42 39 40 41 sylancl φHFin
43 rnfi HFinranHFin
44 42 43 syl φranHFin
45 fnchoice ranHFinhhFnranHwranHwhww
46 44 45 syl φhhFnranHwranHwhww
47 simprl φhFnranHwranHwhwwhFnranH
48 ovex 0NV
49 48 mptex j0NyY|tDjyt<ENtBj1EN<ytV
50 9 49 eqeltri HV
51 50 rnex ranHV
52 fnex hFnranHranHVhV
53 47 51 52 sylancl φhFnranHwranHwhwwhV
54 coexg hVHVhHV
55 53 50 54 sylancl φhFnranHwranHwhwwhHV
56 dffn3 hFnranHh:ranHranh
57 47 56 sylib φhFnranHwranHwhwwh:ranHranh
58 nfv wφ
59 nfv whFnranH
60 nfra1 wwranHwhww
61 59 60 nfan whFnranHwranHwhww
62 58 61 nfan wφhFnranHwranHwhww
63 simplrr φhFnranHwranHwhwwwranHwranHwhww
64 simpr φhFnranHwranHwhwwwranHwranH
65 fvelrnb HFn0NwranHa0NHa=w
66 nfv aHj=w
67 nfmpt1 _jj0NyY|tDjyt<ENtBj1EN<yt
68 9 67 nfcxfr _jH
69 nfcv _ja
70 68 69 nffv _jHa
71 nfcv _jw
72 70 71 nfeq jHa=w
73 fveq2 j=aHj=Ha
74 73 eqeq1d j=aHj=wHa=w
75 66 72 74 cbvrexw j0NHj=wa0NHa=w
76 65 75 bitr4di HFn0NwranHj0NHj=w
77 39 76 syl φwranHj0NHj=w
78 77 biimpa φwranHj0NHj=w
79 simp3 φj0NHj=wHj=w
80 simpr φj0Nj0N
81 36 adantr φj0NyY|tDjyt<ENtBj1EN<ytV
82 9 fvmpt2 j0NyY|tDjyt<ENtBj1EN<ytVHj=yY|tDjyt<ENtBj1EN<yt
83 80 81 82 syl2anc φj0NHj=yY|tDjyt<ENtBj1EN<yt
84 nfcv _t0N
85 nfrab1 _ttT|Ftj13E
86 84 85 nfmpt _tj0NtT|Ftj13E
87 6 86 nfcxfr _tD
88 nfcv _tj
89 87 88 nffv _tDj
90 nfcv _tT
91 nfrab1 _ttT|j+13EFt
92 84 91 nfmpt _tj0NtT|j+13EFt
93 7 92 nfcxfr _tB
94 93 88 nffv _tBj
95 90 94 nfdif _tTBj
96 nfv tj0N
97 2 96 nfan tφj0N
98 10 adantr φj0NJComp
99 11 adantr φj0NAC
100 12 3adant1r φj0NfAgAtTft+gtA
101 13 3adant1r φj0NfAgAtTftgtA
102 14 adantlr φj0NytTyA
103 15 adantlr φj0NrTtTrtqAqrqt
104 10 uniexd φJV
105 4 104 eqeltrid φTV
106 105 adantr φj0NTV
107 rabexg TVtT|j+13EFtV
108 106 107 syl φj0NtT|j+13EFtV
109 7 fvmpt2 j0NtT|j+13EFtVBj=tT|j+13EFt
110 80 108 109 syl2anc φj0NBj=tT|j+13EFt
111 eqid tT|j+13EFt=tT|j+13EFt
112 elfzelz j0Nj
113 112 zred j0Nj
114 3re 3
115 3ne0 30
116 114 115 rereccli 13
117 readdcl j13j+13
118 113 116 117 sylancl j0Nj+13
119 118 adantl φj0Nj+13
120 17 rpred φE
121 120 adantr φj0NE
122 119 121 remulcld φj0Nj+13E
123 16 5 eleqtrdi φFJCnK
124 123 adantr φj0NFJCnK
125 1 3 4 111 122 124 rfcnpre3 φj0NtT|j+13EFtClsdJ
126 110 125 eqeltrd φj0NBjClsdJ
127 rabexg TVtT|Ftj13EV
128 106 127 syl φj0NtT|Ftj13EV
129 6 fvmpt2 j0NtT|Ftj13EVDj=tT|Ftj13E
130 80 128 129 syl2anc φj0NDj=tT|Ftj13E
131 eqid tT|Ftj13E=tT|Ftj13E
132 resubcl j13j13
133 113 116 132 sylancl j0Nj13
134 133 adantl φj0Nj13
135 134 121 remulcld φj0Nj13E
136 1 3 4 131 135 124 rfcnpre4 φj0NtT|Ftj13EClsdJ
137 130 136 eqeltrd φj0NDjClsdJ
138 135 adantr φj0NtBjj13E
139 122 adantr φj0NtBjj+13E
140 3 4 5 16 fcnre φF:T
141 140 ad2antrr φj0NtBjF:T
142 ssrab2 tT|j+13EFtT
143 110 142 eqsstrdi φj0NBjT
144 143 sselda φj0NtBjtT
145 141 144 ffvelrnd φj0NtBjFt
146 116 132 mpan2 jj13
147 id jj
148 116 117 mpan2 jj+13
149 3pos 0<3
150 114 149 recgt0ii 0<13
151 116 150 elrpii 13+
152 ltsubrp j13+j13<j
153 151 152 mpan2 jj13<j
154 ltaddrp j13+j<j+13
155 151 154 mpan2 jj<j+13
156 146 147 148 153 155 lttrd jj13<j+13
157 113 156 syl j0Nj13<j+13
158 157 adantl φj0Nj13<j+13
159 17 rpregt0d φE0<E
160 159 adantr φj0NE0<E
161 ltmul1 j13j+13E0<Ej13<j+13j13E<j+13E
162 134 119 160 161 syl3anc φj0Nj13<j+13j13E<j+13E
163 158 162 mpbid φj0Nj13E<j+13E
164 163 adantr φj0NtBjj13E<j+13E
165 110 eleq2d φj0NtBjttT|j+13EFt
166 165 biimpa φj0NtBjttT|j+13EFt
167 rabid ttT|j+13EFttTj+13EFt
168 166 167 sylib φj0NtBjtTj+13EFt
169 168 simprd φj0NtBjj+13EFt
170 138 139 145 164 169 ltletrd φj0NtBjj13E<Ft
171 138 145 ltnled φj0NtBjj13E<Ft¬Ftj13E
172 170 171 mpbid φj0NtBj¬Ftj13E
173 172 intnand φj0NtBj¬tTFtj13E
174 rabid ttT|Ftj13EtTFtj13E
175 173 174 sylnibr φj0NtBj¬ttT|Ftj13E
176 130 adantr φj0NtBjDj=tT|Ftj13E
177 175 176 neleqtrrd φj0NtBj¬tDj
178 177 ex φj0NtBj¬tDj
179 97 178 ralrimi φj0NtBj¬tDj
180 disj BjDj=aBj¬aDj
181 nfcv _aBj
182 89 nfcri taDj
183 182 nfn t¬aDj
184 nfv a¬tDj
185 eleq1 a=taDjtDj
186 185 notbid a=t¬aDj¬tDj
187 181 94 183 184 186 cbvralfw aBj¬aDjtBj¬tDj
188 180 187 bitri BjDj=tBj¬tDj
189 179 188 sylibr φj0NBjDj=
190 eqid TBj=TBj
191 19 nnrpd φN+
192 17 191 rpdivcld φEN+
193 192 adantr φj0NEN+
194 120 19 nndivred φEN
195 116 a1i φ13
196 19 nnge1d φ1N
197 1re 1
198 0lt1 0<1
199 197 198 pm3.2i 10<1
200 199 a1i φ10<1
201 19 nnred φN
202 19 nngt0d φ0<N
203 lediv2 10<1N0<NE0<E1NENE1
204 200 201 202 159 203 syl121anc φ1NENE1
205 196 204 mpbid φENE1
206 17 rpcnd φE
207 206 div1d φE1=E
208 205 207 breqtrd φENE
209 194 120 195 208 18 lelttrd φEN<13
210 209 adantr φj0NEN<13
211 89 95 97 3 4 5 98 99 100 101 102 103 126 137 189 190 193 210 stoweidlem58 φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xt
212 df-rex xAtT0xtxt1tDjxt<ENtBj1EN<xtxxAtT0xtxt1tDjxt<ENtBj1EN<xt
213 211 212 sylib φj0NxxAtT0xtxt1tDjxt<ENtBj1EN<xt
214 simprl φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xtxA
215 simprr1 φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xttT0xtxt1
216 fveq1 y=xyt=xt
217 216 breq2d y=x0yt0xt
218 216 breq1d y=xyt1xt1
219 217 218 anbi12d y=x0ytyt10xtxt1
220 219 ralbidv y=xtT0ytyt1tT0xtxt1
221 220 8 elrab2 xYxAtT0xtxt1
222 214 215 221 sylanbrc φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xtxY
223 simprr2 φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xttDjxt<EN
224 simprr3 φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xttBj1EN<xt
225 223 224 jca φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xttDjxt<ENtBj1EN<xt
226 nfcv _yx
227 nfv ytDjxt<ENtBj1EN<xt
228 216 breq1d y=xyt<ENxt<EN
229 228 ralbidv y=xtDjyt<ENtDjxt<EN
230 216 breq2d y=x1EN<yt1EN<xt
231 230 ralbidv y=xtBj1EN<yttBj1EN<xt
232 229 231 anbi12d y=xtDjyt<ENtBj1EN<yttDjxt<ENtBj1EN<xt
233 226 21 227 232 elrabf xyY|tDjyt<ENtBj1EN<ytxYtDjxt<ENtBj1EN<xt
234 222 225 233 sylanbrc φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xtxyY|tDjyt<ENtBj1EN<yt
235 234 ex φj0NxAtT0xtxt1tDjxt<ENtBj1EN<xtxyY|tDjyt<ENtBj1EN<yt
236 235 eximdv φj0NxxAtT0xtxt1tDjxt<ENtBj1EN<xtxxyY|tDjyt<ENtBj1EN<yt
237 213 236 mpd φj0NxxyY|tDjyt<ENtBj1EN<yt
238 ne0i xyY|tDjyt<ENtBj1EN<ytyY|tDjyt<ENtBj1EN<yt
239 238 exlimiv xxyY|tDjyt<ENtBj1EN<ytyY|tDjyt<ENtBj1EN<yt
240 237 239 syl φj0NyY|tDjyt<ENtBj1EN<yt
241 83 240 eqnetrd φj0NHj
242 241 3adant3 φj0NHj=wHj
243 79 242 eqnetrrd φj0NHj=ww
244 243 3exp φj0NHj=ww
245 244 rexlimdv φj0NHj=ww
246 245 adantr φwranHj0NHj=ww
247 78 246 mpd φwranHw
248 247 adantlr φhFnranHwranHwhwwwranHw
249 rsp wranHwhwwwranHwhww
250 63 64 248 249 syl3c φhFnranHwranHwhwwwranHhww
251 250 ex φhFnranHwranHwhwwwranHhww
252 62 251 ralrimi φhFnranHwranHwhwwwranHhww
253 chfnrn hFnranHwranHhwwranhranH
254 47 252 253 syl2anc φhFnranHwranHwhwwranhranH
255 nfv yφ
256 nfcv _yh
257 nfcv _y0N
258 nfrab1 _yyY|tDjyt<ENtBj1EN<yt
259 257 258 nfmpt _yj0NyY|tDjyt<ENtBj1EN<yt
260 9 259 nfcxfr _yH
261 260 nfrn _yranH
262 256 261 nffn yhFnranH
263 nfv ywhww
264 261 263 nfralw ywranHwhww
265 262 264 nfan yhFnranHwranHwhww
266 255 265 nfan yφhFnranHwranHwhww
267 261 nfuni _yranH
268 fnunirn HFn0NyranHz0NyHz
269 nfcv _jz
270 68 269 nffv _jHz
271 270 nfcri jyHz
272 nfv zyHj
273 fveq2 z=jHz=Hj
274 273 eleq2d z=jyHzyHj
275 271 272 274 cbvrexw z0NyHzj0NyHj
276 268 275 bitrdi HFn0NyranHj0NyHj
277 39 276 syl φyranHj0NyHj
278 277 biimpa φyranHj0NyHj
279 nfv jφ
280 68 nfrn _jranH
281 280 nfuni _jranH
282 281 nfcri jyranH
283 279 282 nfan jφyranH
284 nfv jyY
285 simp1l φyranHj0NyHjφ
286 simp2 φyranHj0NyHjj0N
287 simp3 φyranHj0NyHjyHj
288 83 eleq2d φj0NyHjyyY|tDjyt<ENtBj1EN<yt
289 288 biimpa φj0NyHjyyY|tDjyt<ENtBj1EN<yt
290 rabid yyY|tDjyt<ENtBj1EN<ytyYtDjyt<ENtBj1EN<yt
291 289 290 sylib φj0NyHjyYtDjyt<ENtBj1EN<yt
292 291 simpld φj0NyHjyY
293 285 286 287 292 syl21anc φyranHj0NyHjyY
294 293 3exp φyranHj0NyHjyY
295 283 284 294 rexlimd φyranHj0NyHjyY
296 278 295 mpd φyranHyY
297 296 adantlr φhFnranHwranHwhwwyranHyY
298 297 ex φhFnranHwranHwhwwyranHyY
299 266 267 21 298 ssrd φhFnranHwranHwhwwranHY
300 ssrab2 yA|tT0ytyt1A
301 8 300 eqsstri YA
302 299 301 sstrdi φhFnranHwranHwhwwranHA
303 254 302 sstrd φhFnranHwranHwhwwranhA
304 57 303 fssd φhFnranHwranHwhwwh:ranHA
305 dffn3 HFn0NH:0NranH
306 39 305 sylib φH:0NranH
307 306 adantr φhFnranHwranHwhwwH:0NranH
308 fco h:ranHAH:0NranHhH:0NA
309 304 307 308 syl2anc φhFnranHwranHwhwwhH:0NA
310 nfcv _jh
311 310 280 nffn jhFnranH
312 nfv jwhww
313 280 312 nfralw jwranHwhww
314 311 313 nfan jhFnranHwranHwhww
315 279 314 nfan jφhFnranHwranHwhww
316 simpll φhFnranHwranHwhwwj0Nφ
317 simpr φhFnranHwranHwhwwj0Nj0N
318 39 ad2antrr φhFnranHwranHwhwwj0NHFn0N
319 fvco2 HFn0Nj0NhHj=hHj
320 318 319 sylancom φhFnranHwranHwhwwj0NhHj=hHj
321 simplrr φhFnranHwranHwhwwj0NwranHwhww
322 fnfun HFn0NFunH
323 39 322 syl φFunH
324 323 ad2antrr φhFnranHwranHwhwwj0NFunH
325 39 fndmd φdomH=0N
326 325 adantr φj0NdomH=0N
327 80 326 eleqtrrd φj0NjdomH
328 327 adantlr φhFnranHwranHwhwwj0NjdomH
329 fvelrn FunHjdomHHjranH
330 324 328 329 syl2anc φhFnranHwranHwhwwj0NHjranH
331 321 330 jca φhFnranHwranHwhwwj0NwranHwhwwHjranH
332 241 adantlr φhFnranHwranHwhwwj0NHj
333 neeq1 w=HjwHj
334 fveq2 w=Hjhw=hHj
335 id w=Hjw=Hj
336 334 335 eleq12d w=HjhwwhHjHj
337 333 336 imbi12d w=HjwhwwHjhHjHj
338 337 rspccva wranHwhwwHjranHHjhHjHj
339 331 332 338 sylc φhFnranHwranHwhwwj0NhHjHj
340 320 339 eqeltrd φhFnranHwranHwhwwj0NhHjHj
341 256 260 nfco _yhH
342 nfcv _yj
343 341 342 nffv _yhHj
344 nfv yφj0N
345 260 342 nffv _yHj
346 343 345 nfel yhHjHj
347 344 346 nfan yφj0NhHjHj
348 343 21 nfel yhHjY
349 347 348 nfim yφj0NhHjHjhHjY
350 eleq1 y=hHjyHjhHjHj
351 350 anbi2d y=hHjφj0NyHjφj0NhHjHj
352 eleq1 y=hHjyYhHjY
353 351 352 imbi12d y=hHjφj0NyHjyYφj0NhHjHjhHjY
354 343 349 353 292 vtoclgf hHjHjφj0NhHjHjhHjY
355 354 anabsi7 φj0NhHjHjhHjY
356 316 317 340 355 syl21anc φhFnranHwranHwhwwj0NhHjY
357 8 eleq2i hHjYhHjyA|tT0ytyt1
358 nfcv _yA
359 nfcv _yT
360 nfcv _y0
361 nfcv _y
362 nfcv _yt
363 343 362 nffv _yhHjt
364 360 361 363 nfbr y0hHjt
365 nfcv _y1
366 363 361 365 nfbr yhHjt1
367 364 366 nfan y0hHjthHjt1
368 359 367 nfralw ytT0hHjthHjt1
369 nfcv _ty
370 nfcv _th
371 nfra1 ttDjyt<EN
372 nfra1 ttBj1EN<yt
373 371 372 nfan ttDjyt<ENtBj1EN<yt
374 nfra1 ttT0ytyt1
375 nfcv _tA
376 374 375 nfrabw _tyA|tT0ytyt1
377 8 376 nfcxfr _tY
378 373 377 nfrabw _tyY|tDjyt<ENtBj1EN<yt
379 84 378 nfmpt _tj0NyY|tDjyt<ENtBj1EN<yt
380 9 379 nfcxfr _tH
381 370 380 nfco _thH
382 381 88 nffv _thHj
383 369 382 nfeq ty=hHj
384 fveq1 y=hHjyt=hHjt
385 384 breq2d y=hHj0yt0hHjt
386 384 breq1d y=hHjyt1hHjt1
387 385 386 anbi12d y=hHj0ytyt10hHjthHjt1
388 383 387 ralbid y=hHjtT0ytyt1tT0hHjthHjt1
389 343 358 368 388 elrabf hHjyA|tT0ytyt1hHjAtT0hHjthHjt1
390 357 389 bitri hHjYhHjAtT0hHjthHjt1
391 356 390 sylib φhFnranHwranHwhwwj0NhHjAtT0hHjthHjt1
392 391 simprd φhFnranHwranHwhwwj0NtT0hHjthHjt1
393 nfcv _yDj
394 nfcv _y<
395 nfcv _yEN
396 363 394 395 nfbr yhHjt<EN
397 393 396 nfralw ytDjhHjt<EN
398 347 397 nfim yφj0NhHjHjtDjhHjt<EN
399 384 breq1d y=hHjyt<ENhHjt<EN
400 383 399 ralbid y=hHjtDjyt<ENtDjhHjt<EN
401 351 400 imbi12d y=hHjφj0NyHjtDjyt<ENφj0NhHjHjtDjhHjt<EN
402 291 simprd φj0NyHjtDjyt<ENtBj1EN<yt
403 402 simpld φj0NyHjtDjyt<EN
404 343 398 401 403 vtoclgf hHjHjφj0NhHjHjtDjhHjt<EN
405 404 anabsi7 φj0NhHjHjtDjhHjt<EN
406 316 317 340 405 syl21anc φhFnranHwranHwhwwj0NtDjhHjt<EN
407 nfcv _yBj
408 nfcv _y1EN
409 408 394 363 nfbr y1EN<hHjt
410 407 409 nfralw ytBj1EN<hHjt
411 347 410 nfim yφj0NhHjHjtBj1EN<hHjt
412 384 breq2d y=hHj1EN<yt1EN<hHjt
413 383 412 ralbid y=hHjtBj1EN<yttBj1EN<hHjt
414 351 413 imbi12d y=hHjφj0NyHjtBj1EN<ytφj0NhHjHjtBj1EN<hHjt
415 402 simprd φj0NyHjtBj1EN<yt
416 343 411 414 415 vtoclgf hHjHjφj0NhHjHjtBj1EN<hHjt
417 416 anabsi7 φj0NhHjHjtBj1EN<hHjt
418 316 317 340 417 syl21anc φhFnranHwranHwhwwj0NtBj1EN<hHjt
419 392 406 418 3jca φhFnranHwranHwhwwj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
420 419 ex φhFnranHwranHwhwwj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
421 315 420 ralrimi φhFnranHwranHwhwwj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
422 309 421 jca φhFnranHwranHwhwwhH:0NAj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
423 feq1 x=hHx:0NAhH:0NA
424 nfcv _jx
425 310 68 nfco _jhH
426 424 425 nfeq jx=hH
427 nfcv _tx
428 427 381 nfeq tx=hH
429 fveq1 x=hHxj=hHj
430 429 fveq1d x=hHxjt=hHjt
431 430 breq2d x=hH0xjt0hHjt
432 430 breq1d x=hHxjt1hHjt1
433 431 432 anbi12d x=hH0xjtxjt10hHjthHjt1
434 428 433 ralbid x=hHtT0xjtxjt1tT0hHjthHjt1
435 430 breq1d x=hHxjt<ENhHjt<EN
436 428 435 ralbid x=hHtDjxjt<ENtDjhHjt<EN
437 430 breq2d x=hH1EN<xjt1EN<hHjt
438 428 437 ralbid x=hHtBj1EN<xjttBj1EN<hHjt
439 434 436 438 3anbi123d x=hHtT0xjtxjt1tDjxjt<ENtBj1EN<xjttT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
440 426 439 ralbid x=hHj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjtj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
441 423 440 anbi12d x=hHx:0NAj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjthH:0NAj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjt
442 441 spcegv hHVhH:0NAj0NtT0hHjthHjt1tDjhHjt<ENtBj1EN<hHjtxx:0NAj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjt
443 55 422 442 sylc φhFnranHwranHwhwwxx:0NAj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjt
444 46 443 exlimddv φxx:0NAj0NtT0xjtxjt1tDjxjt<ENtBj1EN<xjt