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

Theorem stoweidlem31 38004
 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 is a finite subset of , indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on . Here M is used to represent m in the paper, is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem31.1
stoweidlem31.2
stoweidlem31.3
stoweidlem31.4
stoweidlem31.5
stoweidlem31.6
stoweidlem31.7
stoweidlem31.8
stoweidlem31.9
stoweidlem31.10
stoweidlem31.11
stoweidlem31.12
stoweidlem31.13
stoweidlem31.14
Assertion
Ref Expression
stoweidlem31
Distinct variable groups:   ,,,,   ,   ,   ,   ,,,,   ,,,,   ,,,,   ,,,   ,,,   ,,,   ,,,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,,,,,)   (,,)   (,,,,,)   (,,,)   (,,,)   (,,,)   (,)   (,,,,)   (,,,,,,)   ()   (,,,,,,)   (,,,,)

Proof of Theorem stoweidlem31
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem31.14 . . 3
2 fnchoice 37413 . . 3
31, 2syl 17 . 2
4 vex 3034 . . . . 5
5 stoweidlem31.6 . . . . . . 7
6 stoweidlem31.12 . . . . . . . . 9
7 stoweidlem31.7 . . . . . . . . 9
86, 7ssexd 4543 . . . . . . . 8
9 mptexg 6151 . . . . . . . 8
108, 9syl 17 . . . . . . 7
115, 10syl5eqel 2553 . . . . . 6
12 vex 3034 . . . . . 6
13 coexg 6763 . . . . . 6
1411, 12, 13sylancl 675 . . . . 5
15 coexg 6763 . . . . 5
164, 14, 15sylancr 676 . . . 4
18 simprl 772 . . . . . 6
19 stoweidlem31.1 . . . . . . . . 9
20 nfcv 2612 . . . . . . . . . . 11
21 nfcv 2612 . . . . . . . . . . . . . 14
22 nfrab1 2957 . . . . . . . . . . . . . 14
2321, 22nfmpt 4484 . . . . . . . . . . . . 13
245, 23nfcxfr 2610 . . . . . . . . . . . 12
2524nfrn 5083 . . . . . . . . . . 11
2620, 25nffn 5682 . . . . . . . . . 10
27 nfv 1769 . . . . . . . . . . 11
2825, 27nfral 2789 . . . . . . . . . 10
2926, 28nfan 2031 . . . . . . . . 9
3019, 29nfan 2031 . . . . . . . 8
31 fvelrnb 5926 . . . . . . . . . . . . 13
3218, 31syl 17 . . . . . . . . . . . 12
3332biimpa 492 . . . . . . . . . . 11
34 nfv 1769 . . . . . . . . . . . . . 14
35 nfv 1769 . . . . . . . . . . . . . . 15
36 nfra1 2785 . . . . . . . . . . . . . . 15
3735, 36nfan 2031 . . . . . . . . . . . . . 14
3834, 37nfan 2031 . . . . . . . . . . . . 13
39 nfv 1769 . . . . . . . . . . . . 13
4038, 39nfan 2031 . . . . . . . . . . . 12
41 simp3 1032 . . . . . . . . . . . . . 14
42 simp1ll 1093 . . . . . . . . . . . . . . 15
43 simplrr 779 . . . . . . . . . . . . . . . 16
44433ad2ant1 1051 . . . . . . . . . . . . . . 15
45 simp2 1031 . . . . . . . . . . . . . . 15
46 simp3 1032 . . . . . . . . . . . . . . . . 17
47 3simpc 1029 . . . . . . . . . . . . . . . . . 18
48 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
49 stoweidlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . 25
50 stoweidlem31.13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
51 rabexg 4549 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5250, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5352a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 25
5449, 53ralrimi 2800 . . . . . . . . . . . . . . . . . . . . . . . 24
555fnmpt 5714 . . . . . . . . . . . . . . . . . . . . . . . 24
5654, 55syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
5756adantr 472 . . . . . . . . . . . . . . . . . . . . . 22
58 fvelrnb 5926 . . . . . . . . . . . . . . . . . . . . . . 23
59 nfmpt1 4485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
605, 59nfcxfr 2610 . . . . . . . . . . . . . . . . . . . . . . . . . 26
61 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6260, 61nffv 5886 . . . . . . . . . . . . . . . . . . . . . . . . 25
63 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . 25
6462, 63nfeq 2623 . . . . . . . . . . . . . . . . . . . . . . . 24
65 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . 24
66 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . 25
6766eqeq1d 2473 . . . . . . . . . . . . . . . . . . . . . . . 24
6864, 65, 67cbvrex 3002 . . . . . . . . . . . . . . . . . . . . . . 23
6958, 68syl6bb 269 . . . . . . . . . . . . . . . . . . . . . 22
7057, 69syl 17 . . . . . . . . . . . . . . . . . . . . 21
7148, 70mpbid 215 . . . . . . . . . . . . . . . . . . . 20
7260nfrn 5083 . . . . . . . . . . . . . . . . . . . . . . 23
7372nfcri 2606 . . . . . . . . . . . . . . . . . . . . . 22
7449, 73nfan 2031 . . . . . . . . . . . . . . . . . . . . 21
75 nfv 1769 . . . . . . . . . . . . . . . . . . . . 21
76 simp3 1032 . . . . . . . . . . . . . . . . . . . . . . . 24
77 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
7850adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7978, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
805fvmpt2 5972 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8177, 79, 80syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
827sselda 3418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
83 stoweidlem31.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8483rabeq2i 3028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
8582, 84sylib 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
8685simprd 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
87 stoweidlem31.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
88 stoweidlem31.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
8988nnrpd 11362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9087, 89rpdivcld 11381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9190adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92 breq2 4399 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9392ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
94 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
9594breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
9695ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
9793, 963anbi23d 1368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9897rexbidv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9998rspccva 3135 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10086, 91, 99syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
101 nfv 1769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10219, 101nfan 2031 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
103 nfcv 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10422, 103nfne 2742 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
105 3simpc 1029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
106 rabid 2953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
107105, 106sylibr 217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
108 ne0i 3728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1101093exp 1230 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111102, 104, 110rexlimd 2866 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
112100, 111mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11381, 112eqnetrd 2710 . . . . . . . . . . . . . . . . . . . . . . . . 25
1141133adant3 1050 . . . . . . . . . . . . . . . . . . . . . . . 24
11576, 114eqnetrrd 2711 . . . . . . . . . . . . . . . . . . . . . . 23
1161153adant1r 1285 . . . . . . . . . . . . . . . . . . . . . 22
1171163exp 1230 . . . . . . . . . . . . . . . . . . . . 21
11874, 75, 117rexlimd 2866 . . . . . . . . . . . . . . . . . . . 20
11971, 118mpd 15 . . . . . . . . . . . . . . . . . . 19
1201193adant2 1049 . . . . . . . . . . . . . . . . . 18
121 rspa 2774 . . . . . . . . . . . . . . . . . 18
12247, 120, 121sylc 61 . . . . . . . . . . . . . . . . 17
12346, 122jca 541 . . . . . . . . . . . . . . . 16
124 vex 3034 . . . . . . . . . . . . . . . . . 18
1255elrnmpt 5087 . . . . . . . . . . . . . . . . . 18
126124, 125ax-mp 5 . . . . . . . . . . . . . . . . 17
12746, 126sylib 201 . . . . . . . . . . . . . . . 16
128 nfv 1769 . . . . . . . . . . . . . . . . . 18
12973, 128nfan 2031 . . . . . . . . . . . . . . . . 17
130 nfv 1769 . . . . . . . . . . . . . . . . 17
131 simp1r 1055 . . . . . . . . . . . . . . . . . . 19
132 simp3 1032 . . . . . . . . . . . . . . . . . . 19
133 simpl 464 . . . . . . . . . . . . . . . . . . . . . 22
134 simpr 468 . . . . . . . . . . . . . . . . . . . . . 22
135133, 134eleqtrd 2551 . . . . . . . . . . . . . . . . . . . . 21
136 elrabi 3181 . . . . . . . . . . . . . . . . . . . . . 22
137 fveq1 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
138137breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
139137breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
140138, 139anbi12d 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
141140ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
142137breq1d 4405 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
143142ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
144137breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
145144ralbidv 2829 . . . . . . . . . . . . . . . . . . . . . . . . . 26
146141, 143, 1453anbi123d 1365 . . . . . . . . . . . . . . . . . . . . . . . . 25
147146elrab 3184 . . . . . . . . . . . . . . . . . . . . . . . 24
148147simprbi 471 . . . . . . . . . . . . . . . . . . . . . . 23
149148simp1d 1042 . . . . . . . . . . . . . . . . . . . . . 22
150141elrab 3184 . . . . . . . . . . . . . . . . . . . . . 22
151136, 149, 150sylanbrc 677 . . . . . . . . . . . . . . . . . . . . 21
152135, 151syl 17 . . . . . . . . . . . . . . . . . . . 20
153 stoweidlem31.4 . . . . . . . . . . . . . . . . . . . 20
154152, 153syl6eleqr 2560 . . . . . . . . . . . . . . . . . . 19
155131, 132, 154syl2anc 673 . . . . . . . . . . . . . . . . . 18
1561553exp 1230 . . . . . . . . . . . . . . . . 17
157129, 130, 156rexlimd 2866 . . . . . . . . . . . . . . . 16
158123, 127, 157sylc 61 . . . . . . . . . . . . . . 15
15942, 44, 45, 158syl3anc 1292 . . . . . . . . . . . . . 14
16041, 159eqeltrrd 2550 . . . . . . . . . . . . 13
1611603exp 1230 . . . . . . . . . . . 12
16240, 161reximdai 2853 . . . . . . . . . . 11
16333, 162mpd 15 . . . . . . . . . 10
164 nfv 1769 . . . . . . . . . . 11
165 idd 24 . . . . . . . . . . . 12
166165a1i 11 . . . . . . . . . . 11
16740, 164, 166rexlimd 2866 . . . . . . . . . 10
168163, 167mpd 15 . . . . . . . . 9
169168ex 441 . . . . . . . 8
17030, 169ralrimi 2800 . . . . . . 7
171 dfss3 3408 . . . . . . . 8
172 nfrab1 2957 . . . . . . . . . . 11
173153, 172nfcxfr 2610 . . . . . . . . . 10
174173nfcri 2606 . . . . . . . . 9
175 nfv 1769 . . . . . . . . 9
176 eleq1 2537 . . . . . . . . 9
177174, 175, 176cbvral 3001 . . . . . . . 8
178171, 177bitri 257 . . . . . . 7
179170, 178sylibr 217 . . . . . 6
180 df-f 5593 . . . . . 6
18118, 179, 180sylanbrc 677 . . . . 5
182 dffn3 5748 . . . . . . . 8
18356, 182sylib 201 . . . . . . 7
184183adantr 472 . . . . . 6
185 stoweidlem31.9 . . . . . . . 8
186 f1of 5828 . . . . . . . 8
187185, 186syl 17 . . . . . . 7
188187adantr 472 . . . . . 6
189 fco 5751 . . . . . 6
190184, 188, 189syl2anc 673 . . . . 5
191 fco 5751 . . . . 5
192181, 190, 191syl2anc 673 . . . 4
193 fvco3 5957 . . . . . . . . 9
194190, 193sylan 479 . . . . . . . 8
195 simpll 768 . . . . . . . . 9
196 simplrr 779 . . . . . . . . 9
197190fnvinran 37398 . . . . . . . . 9
198 simp3 1032 . . . . . . . . . 10
199 nfv 1769 . . . . . . . . . . . . 13
20034, 36, 199nf3an 2033 . . . . . . . . . . . 12
201 nfv 1769 . . . . . . . . . . . 12
202200, 201nfim 2023 . . . . . . . . . . 11
203 eleq1 2537 . . . . . . . . . . . . 13
2042033anbi3d 1371 . . . . . . . . . . . 12
205 fveq2 5879 . . . . . . . . . . . . 13
206 id 22 . . . . . . . . . . . . 13
207205, 206eleq12d 2543 . . . . . . . . . . . 12
208204, 207imbi12d 327 . . . . . . . . . . 11
209202, 208, 122vtoclg1f 3092 . . . . . . . . . 10
210198, 209mpcom 36 . . . . . . . . 9
211195, 196, 197, 210syl3anc 1292 . . . . . . . 8
212194, 211eqeltrd 2549 . . . . . . 7
213 fvco3 5957 . . . . . . . . . . . 12
214187, 213sylan 479 . . . . . . . . . . 11
215187fnvinran 37398 . . . . . . . . . . . 12
21650adantr 472 . . . . . . . . . . . . 13
217 rabexg 4549 . . . . . . . . . . . . 13
218216, 217syl 17 . . . . . . . . . . . 12
219 raleq 2973 . . . . . . . . . . . . . . 15
2202193anbi2d 1370 . . . . . . . . . . . . . 14
221220rabbidv 3022 . . . . . . . . . . . . 13
222221, 5fvmptg 5961 . . . . . . . . . . . 12
223215, 218, 222syl2anc 673 . . . . . . . . . . 11
224214, 223eqtrd 2505 . . . . . . . . . 10
225224adantlr 729 . . . . . . . . 9
226225eleq2d 2534 . . . . . . . 8
227 nfcv 2612 . . . . . . . . . . . . . 14
22824, 227nfco 5005 . . . . . . . . . . . . 13
22920, 228nfco 5005 . . . . . . . . . . . 12
230 nfcv 2612 . . . . . . . . . . . 12
231229, 230nffv 5886 . . . . . . . . . . 11
232 nfcv 2612 . . . . . . . . . . 11
233 nfcv 2612 . . . . . . . . . . . . 13
234 nfcv 2612 . . . . . . . . . . . . . . 15
235 nfcv 2612 . . . . . . . . . . . . . . 15
236 nfcv 2612 . . . . . . . . . . . . . . . 16
237231, 236nffv 5886 . . . . . . . . . . . . . . 15
238234, 235, 237nfbr 4440 . . . . . . . . . . . . . 14
239 nfcv 2612 . . . . . . . . . . . . . . 15
240237, 235, 239nfbr 4440 . . . . . . . . . . . . . 14
241238, 240nfan 2031 . . . . . . . . . . . . 13
242233, 241nfral 2789 . . . . . . . . . . . 12
243 nfcv 2612 . . . . . . . . . . . . 13
244 nfcv 2612 . . . . . . . . . . . . . 14
245 nfcv 2612 . . . . . . . . . . . . . 14
246237, 244, 245nfbr 4440 . . . . . . . . . . . . 13
247243, 246nfral 2789 . . . . . . . . . . . 12
248 nfcv 2612 . . . . . . . . . . . . 13
249 nfcv 2612 . . . . . . . . . . . . . 14
250249, 244, 237nfbr 4440 . . . . . . . . . . . . 13
251248, 250nfral 2789 . . . . . . . . . . . 12
252242, 247, 251nf3an 2033 . . . . . . . . . . 11
253 nfcv 2612 . . . . . . . . . . . . . 14
254 nfcv 2612 . . . . . . . . . . . . . . . 16
255 nfcv 2612 . . . . . . . . . . . . . . . . . . 19
256 nfra1 2785 . . . . . . . . . . . . . . . . . . . . 21
257 nfra1 2785 . . . . . . . . . . . . . . . . . . . . 21
258 nfra1 2785 . . . . . . . . . . . . . . . . . . . . 21
259256, 257, 258nf3an 2033 . . . . . . . . . . . . . . . . . . . 20
260 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
261259, 260nfrab 2958 . . . . . . . . . . . . . . . . . . 19
262255, 261nfmpt 4484 . . . . . . . . . . . . . . . . . 18
2635, 262nfcxfr 2610 . . . . . . . . . . . . . . . . 17
264 nfcv 2612 . . . . . . . . . . . . . . . . 17
265263, 264nfco 5005 . . . . . . . . . . . . . . . 16
266254, 265nfco 5005 . . . . . . . . . . . . . . 15
267 nfcv 2612 . . . . . . . . . . . . . . 15
268266, 267nffv 5886 . . . . . . . . . . . . . 14
269253, 268nfeq 2623 . . . . . . . . . . . . 13
270 fveq1 5878 . . . . . . . . . . . . . . 15
271270breq2d 4407 . . . . . . . . . . . . . 14
272270breq1d 4405 . . . . . . . . . . . . . 14
273271, 272anbi12d 725 . . . . . . . . . . . . 13
274269, 273ralbid 2826 . . . . . . . . . . . 12
275270breq1d 4405 . . . . . . . . . . . . 13
276269, 275ralbid 2826 . . . . . . . . . . . 12
277270breq2d 4407 . . . . . . . . . . . . 13
278269, 277ralbid 2826 . . . . . . . . . . . 12
279274, 276, 2783anbi123d 1365 . . . . . . . . . . 11
280231, 232, 252, 279elrabf 3182 . . . . . . . . . 10
281280simprbi 471 . . . . . . . . 9
282281simp2d 1043 . . . . . . . 8
283226, 282syl6bi 236 . . . . . . 7
284212, 283mpd 15 . . . . . 6
285 stoweidlem31.2 . . . . . . . . 9
286263nfrn 5083 . . . . . . . . . . 11
287254, 286nffn 5682 . . . . . . . . . 10
288 nfv 1769 . . . . . . . . . . 11
289286, 288nfral 2789 . . . . . . . . . 10
290287, 289nfan 2031 . . . . . . . . 9
291285, 290nfan 2031 . . . . . . . 8
292 nfv 1769 . . . . . . . 8
293291, 292nfan 2031 . . . . . . 7
294 stoweidlem31.11 . . . . . . . . . . 11
295294ad3antrrr 744 . . . . . . . . . 10
296 simpr 468 . . . . . . . . . 10
297295, 296sseldd 3419 . . . . . . . . 9
298281simp3d 1044 . . . . . . . . . . . 12
299226, 298syl6bi 236 . . . . . . . . . . 11
300212, 299mpd 15 . . . . . . . . . 10
301300r19.21bi 2776 . . . . . . . . 9
302297, 301syldan 478 . . . . . . . 8
303302ex 441 . . . . . . 7
304293, 303ralrimi 2800 . . . . . 6
305284, 304jca 541 . . . . 5
306305ralrimiva 2809 . . . 4
307192, 306jca 541 . . 3
308 feq1 5720 . . . . 5
309 nfcv 2612 . . . . . . . . 9
310309, 266nfeq 2623 . . . . . . . 8
311 fveq1 5878 . . . . . . . . . 10
312311fveq1d 5881 . . . . . . . . 9
313312breq1d 4405 . . . . . . . 8
314310, 313ralbid 2826 . . . . . . 7
315312breq2d 4407 . . . . . . . 8
316310, 315ralbid 2826 . . . . . . 7
317314, 316anbi12d 725 . . . . . 6