Metamath Proof Explorer


Theorem stoweidlem31

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that R is a finite subset of V , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here M is used to represent m in the paper, E is used to represent ε in the paper, v_i is used to represent V(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem31.1 hφ
stoweidlem31.2 tφ
stoweidlem31.3 wφ
stoweidlem31.4 Y=hA|tT0htht1
stoweidlem31.5 V=wJ|e+hAtT0htht1twht<etTU1e<ht
stoweidlem31.6 G=wRhA|tT0htht1twht<EMtTU1EM<ht
stoweidlem31.7 φRV
stoweidlem31.8 φM
stoweidlem31.9 φv:1M1-1 ontoR
stoweidlem31.10 φE+
stoweidlem31.11 φBTU
stoweidlem31.12 φVV
stoweidlem31.13 φAV
stoweidlem31.14 φranGFin
Assertion stoweidlem31 φxx:1MYi1Mtvixit<EMtB1EM<xit

Proof

Step Hyp Ref Expression
1 stoweidlem31.1 hφ
2 stoweidlem31.2 tφ
3 stoweidlem31.3 wφ
4 stoweidlem31.4 Y=hA|tT0htht1
5 stoweidlem31.5 V=wJ|e+hAtT0htht1twht<etTU1e<ht
6 stoweidlem31.6 G=wRhA|tT0htht1twht<EMtTU1EM<ht
7 stoweidlem31.7 φRV
8 stoweidlem31.8 φM
9 stoweidlem31.9 φv:1M1-1 ontoR
10 stoweidlem31.10 φE+
11 stoweidlem31.11 φBTU
12 stoweidlem31.12 φVV
13 stoweidlem31.13 φAV
14 stoweidlem31.14 φranGFin
15 fnchoice ranGFinllFnranGbranGblbb
16 14 15 syl φllFnranGbranGblbb
17 vex lV
18 12 7 ssexd φRV
19 mptexg RVwRhA|tT0htht1twht<EMtTU1EM<htV
20 18 19 syl φwRhA|tT0htht1twht<EMtTU1EM<htV
21 6 20 eqeltrid φGV
22 vex vV
23 coexg GVvVGvV
24 21 22 23 sylancl φGvV
25 coexg lVGvVlGvV
26 17 24 25 sylancr φlGvV
27 26 adantr φlFnranGbranGblbblGvV
28 simprl φlFnranGbranGblbblFnranG
29 nfcv _hl
30 nfcv _hR
31 nfrab1 _hhA|tT0htht1twht<EMtTU1EM<ht
32 30 31 nfmpt _hwRhA|tT0htht1twht<EMtTU1EM<ht
33 6 32 nfcxfr _hG
34 33 nfrn _hranG
35 29 34 nffn hlFnranG
36 nfv hblbb
37 34 36 nfralw hbranGblbb
38 35 37 nfan hlFnranGbranGblbb
39 1 38 nfan hφlFnranGbranGblbb
40 fvelrnb lFnranGhranlbranGlb=h
41 28 40 syl φlFnranGbranGblbbhranlbranGlb=h
42 41 biimpa φlFnranGbranGblbbhranlbranGlb=h
43 nfv bφ
44 nfv blFnranG
45 nfra1 bbranGblbb
46 44 45 nfan blFnranGbranGblbb
47 43 46 nfan bφlFnranGbranGblbb
48 nfv bhranl
49 47 48 nfan bφlFnranGbranGblbbhranl
50 simp3 φlFnranGbranGblbbhranlbranGlb=hlb=h
51 simp1ll φlFnranGbranGblbbhranlbranGlb=hφ
52 simplrr φlFnranGbranGblbbhranlbranGblbb
53 52 3ad2ant1 φlFnranGbranGblbbhranlbranGlb=hbranGblbb
54 simp2 φlFnranGbranGblbbhranlbranGlb=hbranG
55 simp3 φbranGblbbbranGbranG
56 3simpc φbranGblbbbranGbranGblbbbranG
57 simpr φbranGbranG
58 rabexg AVhA|tT0htht1twht<EMtTU1EM<htV
59 13 58 syl φhA|tT0htht1twht<EMtTU1EM<htV
60 59 a1d φwRhA|tT0htht1twht<EMtTU1EM<htV
61 3 60 ralrimi φwRhA|tT0htht1twht<EMtTU1EM<htV
62 6 fnmpt wRhA|tT0htht1twht<EMtTU1EM<htVGFnR
63 61 62 syl φGFnR
64 63 adantr φbranGGFnR
65 fvelrnb GFnRbranGuRGu=b
66 nfmpt1 _wwRhA|tT0htht1twht<EMtTU1EM<ht
67 6 66 nfcxfr _wG
68 nfcv _wu
69 67 68 nffv _wGu
70 nfcv _wb
71 69 70 nfeq wGu=b
72 nfv uGw=b
73 fveq2 u=wGu=Gw
74 73 eqeq1d u=wGu=bGw=b
75 71 72 74 cbvrexw uRGu=bwRGw=b
76 65 75 bitrdi GFnRbranGwRGw=b
77 64 76 syl φbranGbranGwRGw=b
78 57 77 mpbid φbranGwRGw=b
79 67 nfrn _wranG
80 79 nfcri wbranG
81 3 80 nfan wφbranG
82 nfv wb
83 simp3 φwRGw=bGw=b
84 simpr φwRwR
85 13 adantr φwRAV
86 85 58 syl φwRhA|tT0htht1twht<EMtTU1EM<htV
87 6 fvmpt2 wRhA|tT0htht1twht<EMtTU1EM<htVGw=hA|tT0htht1twht<EMtTU1EM<ht
88 84 86 87 syl2anc φwRGw=hA|tT0htht1twht<EMtTU1EM<ht
89 7 sselda φwRwV
90 5 rabeq2i wVwJe+hAtT0htht1twht<etTU1e<ht
91 89 90 sylib φwRwJe+hAtT0htht1twht<etTU1e<ht
92 91 simprd φwRe+hAtT0htht1twht<etTU1e<ht
93 8 nnrpd φM+
94 10 93 rpdivcld φEM+
95 94 adantr φwREM+
96 breq2 e=EMht<eht<EM
97 96 ralbidv e=EMtwht<etwht<EM
98 oveq2 e=EM1e=1EM
99 98 breq1d e=EM1e<ht1EM<ht
100 99 ralbidv e=EMtTU1e<httTU1EM<ht
101 97 100 3anbi23d e=EMtT0htht1twht<etTU1e<httT0htht1twht<EMtTU1EM<ht
102 101 rexbidv e=EMhAtT0htht1twht<etTU1e<hthAtT0htht1twht<EMtTU1EM<ht
103 102 rspccva e+hAtT0htht1twht<etTU1e<htEM+hAtT0htht1twht<EMtTU1EM<ht
104 92 95 103 syl2anc φwRhAtT0htht1twht<EMtTU1EM<ht
105 nfv hwR
106 1 105 nfan hφwR
107 nfcv _h
108 31 107 nfne hhA|tT0htht1twht<EMtTU1EM<ht
109 3simpc φwRhAtT0htht1twht<EMtTU1EM<hthAtT0htht1twht<EMtTU1EM<ht
110 rabid hhA|tT0htht1twht<EMtTU1EM<hthAtT0htht1twht<EMtTU1EM<ht
111 109 110 sylibr φwRhAtT0htht1twht<EMtTU1EM<hthhA|tT0htht1twht<EMtTU1EM<ht
112 ne0i hhA|tT0htht1twht<EMtTU1EM<hthA|tT0htht1twht<EMtTU1EM<ht
113 111 112 syl φwRhAtT0htht1twht<EMtTU1EM<hthA|tT0htht1twht<EMtTU1EM<ht
114 113 3exp φwRhAtT0htht1twht<EMtTU1EM<hthA|tT0htht1twht<EMtTU1EM<ht
115 106 108 114 rexlimd φwRhAtT0htht1twht<EMtTU1EM<hthA|tT0htht1twht<EMtTU1EM<ht
116 104 115 mpd φwRhA|tT0htht1twht<EMtTU1EM<ht
117 88 116 eqnetrd φwRGw
118 117 3adant3 φwRGw=bGw
119 83 118 eqnetrrd φwRGw=bb
120 119 3adant1r φbranGwRGw=bb
121 120 3exp φbranGwRGw=bb
122 81 82 121 rexlimd φbranGwRGw=bb
123 78 122 mpd φbranGb
124 123 3adant2 φbranGblbbbranGb
125 rspa branGblbbbranGblbb
126 56 124 125 sylc φbranGblbbbranGlbb
127 55 126 jca φbranGblbbbranGbranGlbb
128 vex bV
129 6 elrnmpt bVbranGwRb=hA|tT0htht1twht<EMtTU1EM<ht
130 128 129 ax-mp branGwRb=hA|tT0htht1twht<EMtTU1EM<ht
131 55 130 sylib φbranGblbbbranGwRb=hA|tT0htht1twht<EMtTU1EM<ht
132 nfv wlbb
133 80 132 nfan wbranGlbb
134 nfv wlbY
135 simp1r branGlbbwRb=hA|tT0htht1twht<EMtTU1EM<htlbb
136 simp3 branGlbbwRb=hA|tT0htht1twht<EMtTU1EM<htb=hA|tT0htht1twht<EMtTU1EM<ht
137 simpl lbbb=hA|tT0htht1twht<EMtTU1EM<htlbb
138 simpr lbbb=hA|tT0htht1twht<EMtTU1EM<htb=hA|tT0htht1twht<EMtTU1EM<ht
139 137 138 eleqtrd lbbb=hA|tT0htht1twht<EMtTU1EM<htlbhA|tT0htht1twht<EMtTU1EM<ht
140 elrabi lbhA|tT0htht1twht<EMtTU1EM<htlbA
141 fveq1 h=lbht=lbt
142 141 breq2d h=lb0ht0lbt
143 141 breq1d h=lbht1lbt1
144 142 143 anbi12d h=lb0htht10lbtlbt1
145 144 ralbidv h=lbtT0htht1tT0lbtlbt1
146 141 breq1d h=lbht<EMlbt<EM
147 146 ralbidv h=lbtwht<EMtwlbt<EM
148 141 breq2d h=lb1EM<ht1EM<lbt
149 148 ralbidv h=lbtTU1EM<httTU1EM<lbt
150 145 147 149 3anbi123d h=lbtT0htht1twht<EMtTU1EM<httT0lbtlbt1twlbt<EMtTU1EM<lbt
151 150 elrab lbhA|tT0htht1twht<EMtTU1EM<htlbAtT0lbtlbt1twlbt<EMtTU1EM<lbt
152 151 simprbi lbhA|tT0htht1twht<EMtTU1EM<httT0lbtlbt1twlbt<EMtTU1EM<lbt
153 152 simp1d lbhA|tT0htht1twht<EMtTU1EM<httT0lbtlbt1
154 145 elrab lbhA|tT0htht1lbAtT0lbtlbt1
155 140 153 154 sylanbrc lbhA|tT0htht1twht<EMtTU1EM<htlbhA|tT0htht1
156 139 155 syl lbbb=hA|tT0htht1twht<EMtTU1EM<htlbhA|tT0htht1
157 156 4 eleqtrrdi lbbb=hA|tT0htht1twht<EMtTU1EM<htlbY
158 135 136 157 syl2anc branGlbbwRb=hA|tT0htht1twht<EMtTU1EM<htlbY
159 158 3exp branGlbbwRb=hA|tT0htht1twht<EMtTU1EM<htlbY
160 133 134 159 rexlimd branGlbbwRb=hA|tT0htht1twht<EMtTU1EM<htlbY
161 127 131 160 sylc φbranGblbbbranGlbY
162 51 53 54 161 syl3anc φlFnranGbranGblbbhranlbranGlb=hlbY
163 50 162 eqeltrrd φlFnranGbranGblbbhranlbranGlb=hhY
164 163 3exp φlFnranGbranGblbbhranlbranGlb=hhY
165 49 164 reximdai φlFnranGbranGblbbhranlbranGlb=hbranGhY
166 42 165 mpd φlFnranGbranGblbbhranlbranGhY
167 nfv bhY
168 idd branGhYhY
169 168 a1i φlFnranGbranGblbbhranlbranGhYhY
170 49 167 169 rexlimd φlFnranGbranGblbbhranlbranGhYhY
171 166 170 mpd φlFnranGbranGblbbhranlhY
172 171 ex φlFnranGbranGblbbhranlhY
173 39 172 ralrimi φlFnranGbranGblbbhranlhY
174 dfss3 ranlYzranlzY
175 nfrab1 _hhA|tT0htht1
176 4 175 nfcxfr _hY
177 176 nfcri hzY
178 nfv zhY
179 eleq1 z=hzYhY
180 177 178 179 cbvralw zranlzYhranlhY
181 174 180 bitri ranlYhranlhY
182 173 181 sylibr φlFnranGbranGblbbranlY
183 df-f l:ranGYlFnranGranlY
184 28 182 183 sylanbrc φlFnranGbranGblbbl:ranGY
185 dffn3 GFnRG:RranG
186 63 185 sylib φG:RranG
187 186 adantr φlFnranGbranGblbbG:RranG
188 f1of v:1M1-1 ontoRv:1MR
189 9 188 syl φv:1MR
190 189 adantr φlFnranGbranGblbbv:1MR
191 fco G:RranGv:1MRGv:1MranG
192 187 190 191 syl2anc φlFnranGbranGblbbGv:1MranG
193 fco l:ranGYGv:1MranGlGv:1MY
194 184 192 193 syl2anc φlFnranGbranGblbblGv:1MY
195 fvco3 Gv:1MranGi1MlGvi=lGvi
196 192 195 sylan φlFnranGbranGblbbi1MlGvi=lGvi
197 simpll φlFnranGbranGblbbi1Mφ
198 simplrr φlFnranGbranGblbbi1MbranGblbb
199 192 ffvelrnda φlFnranGbranGblbbi1MGviranG
200 simp3 φbranGblbbGviranGGviranG
201 nfv bGviranG
202 43 45 201 nf3an bφbranGblbbGviranG
203 nfv blGviGvi
204 202 203 nfim bφbranGblbbGviranGlGviGvi
205 eleq1 b=GvibranGGviranG
206 205 3anbi3d b=GviφbranGblbbbranGφbranGblbbGviranG
207 fveq2 b=Gvilb=lGvi
208 id b=Gvib=Gvi
209 207 208 eleq12d b=GvilbblGviGvi
210 206 209 imbi12d b=GviφbranGblbbbranGlbbφbranGblbbGviranGlGviGvi
211 204 210 126 vtoclg1f GviranGφbranGblbbGviranGlGviGvi
212 200 211 mpcom φbranGblbbGviranGlGviGvi
213 197 198 199 212 syl3anc φlFnranGbranGblbbi1MlGviGvi
214 196 213 eqeltrd φlFnranGbranGblbbi1MlGviGvi
215 fvco3 v:1MRi1MGvi=Gvi
216 189 215 sylan φi1MGvi=Gvi
217 raleq w=vitwht<EMtviht<EM
218 217 3anbi2d w=vitT0htht1twht<EMtTU1EM<httT0htht1tviht<EMtTU1EM<ht
219 218 rabbidv w=vihA|tT0htht1twht<EMtTU1EM<ht=hA|tT0htht1tviht<EMtTU1EM<ht
220 189 ffvelrnda φi1MviR
221 13 adantr φi1MAV
222 rabexg AVhA|tT0htht1tviht<EMtTU1EM<htV
223 221 222 syl φi1MhA|tT0htht1tviht<EMtTU1EM<htV
224 6 219 220 223 fvmptd3 φi1MGvi=hA|tT0htht1tviht<EMtTU1EM<ht
225 216 224 eqtrd φi1MGvi=hA|tT0htht1tviht<EMtTU1EM<ht
226 225 adantlr φlFnranGbranGblbbi1MGvi=hA|tT0htht1tviht<EMtTU1EM<ht
227 226 eleq2d φlFnranGbranGblbbi1MlGviGvilGvihA|tT0htht1tviht<EMtTU1EM<ht
228 nfcv _hv
229 33 228 nfco _hGv
230 29 229 nfco _hlGv
231 nfcv _hi
232 230 231 nffv _hlGvi
233 nfcv _hA
234 nfcv _hT
235 nfcv _h0
236 nfcv _h
237 nfcv _ht
238 232 237 nffv _hlGvit
239 235 236 238 nfbr h0lGvit
240 nfcv _h1
241 238 236 240 nfbr hlGvit1
242 239 241 nfan h0lGvitlGvit1
243 234 242 nfralw htT0lGvitlGvit1
244 nfcv _hvi
245 nfcv _h<
246 nfcv _hEM
247 238 245 246 nfbr hlGvit<EM
248 244 247 nfralw htvilGvit<EM
249 nfcv _hTU
250 nfcv _h1EM
251 250 245 238 nfbr h1EM<lGvit
252 249 251 nfralw htTU1EM<lGvit
253 243 248 252 nf3an htT0lGvitlGvit1tvilGvit<EMtTU1EM<lGvit
254 nfcv _th
255 nfcv _tl
256 nfcv _tR
257 nfra1 ttT0htht1
258 nfra1 ttwht<EM
259 nfra1 ttTU1EM<ht
260 257 258 259 nf3an ttT0htht1twht<EMtTU1EM<ht
261 nfcv _tA
262 260 261 nfrabw _thA|tT0htht1twht<EMtTU1EM<ht
263 256 262 nfmpt _twRhA|tT0htht1twht<EMtTU1EM<ht
264 6 263 nfcxfr _tG
265 nfcv _tv
266 264 265 nfco _tGv
267 255 266 nfco _tlGv
268 nfcv _ti
269 267 268 nffv _tlGvi
270 254 269 nfeq th=lGvi
271 fveq1 h=lGviht=lGvit
272 271 breq2d h=lGvi0ht0lGvit
273 271 breq1d h=lGviht1lGvit1
274 272 273 anbi12d h=lGvi0htht10lGvitlGvit1
275 270 274 ralbid h=lGvitT0htht1tT0lGvitlGvit1
276 271 breq1d h=lGviht<EMlGvit<EM
277 270 276 ralbid h=lGvitviht<EMtvilGvit<EM
278 271 breq2d h=lGvi1EM<ht1EM<lGvit
279 270 278 ralbid h=lGvitTU1EM<httTU1EM<lGvit
280 275 277 279 3anbi123d h=lGvitT0htht1tviht<EMtTU1EM<httT0lGvitlGvit1tvilGvit<EMtTU1EM<lGvit
281 232 233 253 280 elrabf lGvihA|tT0htht1tviht<EMtTU1EM<htlGviAtT0lGvitlGvit1tvilGvit<EMtTU1EM<lGvit
282 281 simprbi lGvihA|tT0htht1tviht<EMtTU1EM<httT0lGvitlGvit1tvilGvit<EMtTU1EM<lGvit
283 282 simp2d lGvihA|tT0htht1tviht<EMtTU1EM<httvilGvit<EM
284 227 283 syl6bi φlFnranGbranGblbbi1MlGviGvitvilGvit<EM
285 214 284 mpd φlFnranGbranGblbbi1MtvilGvit<EM
286 264 nfrn _tranG
287 255 286 nffn tlFnranG
288 nfv tblbb
289 286 288 nfralw tbranGblbb
290 287 289 nfan tlFnranGbranGblbb
291 2 290 nfan tφlFnranGbranGblbb
292 nfv ti1M
293 291 292 nfan tφlFnranGbranGblbbi1M
294 11 ad3antrrr φlFnranGbranGblbbi1MtBBTU
295 simpr φlFnranGbranGblbbi1MtBtB
296 294 295 sseldd φlFnranGbranGblbbi1MtBtTU
297 282 simp3d lGvihA|tT0htht1tviht<EMtTU1EM<httTU1EM<lGvit
298 227 297 syl6bi φlFnranGbranGblbbi1MlGviGvitTU1EM<lGvit
299 214 298 mpd φlFnranGbranGblbbi1MtTU1EM<lGvit
300 299 r19.21bi φlFnranGbranGblbbi1MtTU1EM<lGvit
301 296 300 syldan φlFnranGbranGblbbi1MtB1EM<lGvit
302 301 ex φlFnranGbranGblbbi1MtB1EM<lGvit
303 293 302 ralrimi φlFnranGbranGblbbi1MtB1EM<lGvit
304 285 303 jca φlFnranGbranGblbbi1MtvilGvit<EMtB1EM<lGvit
305 304 ralrimiva φlFnranGbranGblbbi1MtvilGvit<EMtB1EM<lGvit
306 194 305 jca φlFnranGbranGblbblGv:1MYi1MtvilGvit<EMtB1EM<lGvit
307 feq1 x=lGvx:1MYlGv:1MY
308 nfcv _tx
309 308 267 nfeq tx=lGv
310 fveq1 x=lGvxi=lGvi
311 310 fveq1d x=lGvxit=lGvit
312 311 breq1d x=lGvxit<EMlGvit<EM
313 309 312 ralbid x=lGvtvixit<EMtvilGvit<EM
314 311 breq2d x=lGv1EM<xit1EM<lGvit
315 309 314 ralbid x=lGvtB1EM<xittB1EM<lGvit
316 313 315 anbi12d x=lGvtvixit<EMtB1EM<xittvilGvit<EMtB1EM<lGvit
317 316 ralbidv x=lGvi1Mtvixit<EMtB1EM<xiti1MtvilGvit<EMtB1EM<lGvit
318 307 317 anbi12d x=lGvx:1MYi1Mtvixit<EMtB1EM<xitlGv:1MYi1MtvilGvit<EMtB1EM<lGvit
319 318 spcegv lGvVlGv:1MYi1MtvilGvit<EMtB1EM<lGvitxx:1MYi1Mtvixit<EMtB1EM<xit
320 27 306 319 sylc φlFnranGbranGblbbxx:1MYi1Mtvixit<EMtB1EM<xit
321 16 320 exlimddv φxx:1MYi1Mtvixit<EMtB1EM<xit