MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mplbas2 Unicode version

Theorem mplbas2 17728
Description: An alternative expression for the set of polynomials, as the smallest subalgebra of the set of power series that contains all the variable generators. (Contributed by Mario Carneiro, 10-Jan-2015.)
Hypotheses
Ref Expression
mplbas2.p
mplbas2.s
mplbas2.v
mplbas2.a
mplbas2.i
mplbas2.r
Assertion
Ref Expression
mplbas2

Proof of Theorem mplbas2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mplbas2.s . . . . 5
2 mplbas2.i . . . . 5
3 mplbas2.r . . . . 5
41, 2, 3psrassa 17663 . . . 4
5 mplbas2.p . . . . . 6
6 eqid 2454 . . . . . 6
7 eqid 2454 . . . . . 6
85, 1, 6, 7mplbasss 17685 . . . . 5
98a1i 11 . . . 4
10 mplbas2.v . . . . . . . 8
11 crngrng 16831 . . . . . . . . 9
123, 11syl 16 . . . . . . . 8
131, 10, 7, 2, 12mvrf 17674 . . . . . . 7
14 ffn 5679 . . . . . . 7
1513, 14syl 16 . . . . . 6
162adantr 465 . . . . . . . 8
1712adantr 465 . . . . . . . 8
18 simpr 461 . . . . . . . 8
195, 10, 6, 16, 17, 18mvrcl 17705 . . . . . . 7
2019ralrimiva 2831 . . . . . 6
21 ffnfv 5992 . . . . . 6
2215, 20, 21sylanbrc 664 . . . . 5
23 frn 5685 . . . . 5
2422, 23syl 16 . . . 4
25 mplbas2.a . . . . 5
2625, 7aspss 17579 . . . 4
274, 9, 24, 26syl3anc 1219 . . 3
281, 5, 6, 2, 12mplsubrg 17696 . . . 4
291, 5, 6, 2, 12mpllss 17693 . . . 4
30 eqid 2454 . . . . 5
3125, 7, 30aspid 17577 . . . 4
324, 28, 29, 31syl3anc 1219 . . 3
3327, 32sseqtrd 3506 . 2
34 eqid 2454 . . . . . 6
35 eqid 2454 . . . . . 6
36 eqid 2454 . . . . . 6
372adantr 465 . . . . . 6
38 eqid 2454 . . . . . 6
3912adantr 465 . . . . . 6
40 simpr 461 . . . . . 6
415, 34, 35, 36, 37, 6, 38, 39, 40mplcoe1 17721 . . . . 5
42 eqid 2454 . . . . . 6
435mplrng 17708 . . . . . . . . 9
442, 12, 43syl2anc 661 . . . . . . . 8
45 rngabl 16850 . . . . . . . 8
4644, 45syl 16 . . . . . . 7
4746adantr 465 . . . . . 6
48 ovex 6247 . . . . . . . 8
4948rabex 4560 . . . . . . 7
5049a1i 11 . . . . . 6
5124, 8syl6ss 3482 . . . . . . . . . 10
5225, 7aspsubrg 17578 . . . . . . . . . 10
534, 51, 52syl2anc 661 . . . . . . . . 9
545, 1, 6mplval2 17684 . . . . . . . . . . 11
5554subsubrg 17067 . . . . . . . . . 10
5628, 55syl 16 . . . . . . . . 9
5753, 33, 56mpbir2and 913 . . . . . . . 8
58 subrgsubg 17047 . . . . . . . 8
5957, 58syl 16 . . . . . . 7
6059adantr 465 . . . . . 6
615mpllmod 17707 . . . . . . . . . 10
622, 12, 61syl2anc 661 . . . . . . . . 9
6362ad2antrr 725 . . . . . . . 8
6425, 7, 30asplss 17576 . . . . . . . . . . 11
654, 51, 64syl2anc 661 . . . . . . . . . 10
661, 2, 12psrlmod 17648 . . . . . . . . . . 11
67 eqid 2454 . . . . . . . . . . . 12
6854, 30, 67lsslss 17218 . . . . . . . . . . 11
6966, 29, 68syl2anc 661 . . . . . . . . . 10
7065, 33, 69mpbir2and 913 . . . . . . . . 9
7170ad2antrr 725 . . . . . . . 8
72 eqid 2454 . . . . . . . . . . 11
735, 72, 6, 34, 40mplelf 17686 . . . . . . . . . 10
7473ffvelrnda 5966 . . . . . . . . 9
755, 37, 39mplsca 17701 . . . . . . . . . . 11
7675adantr 465 . . . . . . . . . 10
7776fveq2d 5817 . . . . . . . . 9
7874, 77eleqtrd 2544 . . . . . . . 8
792ad2antrr 725 . . . . . . . . . 10
80 eqid 2454 . . . . . . . . . 10
81 eqid 2454 . . . . . . . . . 10
823ad2antrr 725 . . . . . . . . . 10
83 simpr 461 . . . . . . . . . 10
845, 34, 35, 36, 79, 80, 81, 10, 82, 83mplcoe2 17726 . . . . . . . . 9
85 eqid 2454 . . . . . . . . . . 11
8680, 85rngidval 16780 . . . . . . . . . 10
875mplcrng 17709 . . . . . . . . . . . . 13
882, 3, 87syl2anc 661 . . . . . . . . . . . 12
8980crngmgp 16829 . . . . . . . . . . . 12
9088, 89syl 16 . . . . . . . . . . 11
9190ad2antrr 725 . . . . . . . . . 10
9257ad2antrr 725 . . . . . . . . . . 11
9380subrgsubm 17054 . . . . . . . . . . 11
9492, 93syl 16 . . . . . . . . . 10
95 simplll 757 . . . . . . . . . . . 12
9634psrbag 17607 . . . . . . . . . . . . . . . 16
9737, 96syl 16 . . . . . . . . . . . . . . 15
9897biimpa 484 . . . . . . . . . . . . . 14
9998simpld 459 . . . . . . . . . . . . 13
10099ffvelrnda 5966 . . . . . . . . . . . 12
10125, 7aspssid 17580 . . . . . . . . . . . . . . 15
1024, 51, 101syl2anc 661 . . . . . . . . . . . . . 14
103102ad3antrrr 729 . . . . . . . . . . . . 13
10415ad2antrr 725 . . . . . . . . . . . . . 14
105 fnfvelrn 5963 . . . . . . . . . . . . . 14
106104, 105sylan 471 . . . . . . . . . . . . 13
107103, 106sseldd 3471 . . . . . . . . . . . 12
10880, 6mgpbas 16772 . . . . . . . . . . . . 13
109 eqid 2454 . . . . . . . . . . . . . 14
11080, 109mgpplusg 16770 . . . . . . . . . . . . 13
111109subrgmcl 17053 . . . . . . . . . . . . . 14
11257, 111syl3an1 1252 . . . . . . . . . . . . 13
11385subrg1cl 17049 . . . . . . . . . . . . . 14
11457, 113syl 16 . . . . . . . . . . . . 13
115108, 81, 110, 90, 33, 112, 86, 114mulgnn0subcl 15799 . . . . . . . . . . . 12
11695, 100, 107, 115syl3anc 1219 . . . . . . . . . . 11
117 eqid 2454 . . . . . . . . . . 11
118116, 117fmptd 5990 . . . . . . . . . 10
119 mptexg 6072 . . . . . . . . . . . . 13
1202, 119syl 16 . . . . . . . . . . . 12
121120ad2antrr 725 . . . . . . . . . . 11
122 funmpt 5573 . . . . . . . . . . . 12
123122a1i 11 . . . . . . . . . . 11
124 fvex 5823 . . . . . . . . . . . 12
125124a1i 11 . . . . . . . . . . 11
12698simprd 463 . . . . . . . . . . 11
127 elrabi 3224 . . . . . . . . . . . . . . 15
128 elmapi 7368 . . . . . . . . . . . . . . . . 17
129128adantl 466 . . . . . . . . . . . . . . . 16
1302ad2antrr 725 . . . . . . . . . . . . . . . . . 18
131 frnnn0supp 10771 . . . . . . . . . . . . . . . . . 18
132130, 129, 131syl2anc 661 . . . . . . . . . . . . . . . . 17
133 eqimss 3522 . . . . . . . . . . . . . . . . 17
134132, 133syl 16 . . . . . . . . . . . . . . . 16
135 c0ex 9517 . . . . . . . . . . . . . . . . 17
136135a1i 11 . . . . . . . . . . . . . . . 16
137129, 134, 130, 136suppssr 6854 . . . . . . . . . . . . . . 15
138127, 137sylanl2 651 . . . . . . . . . . . . . 14
139138oveq1d 6237 . . . . . . . . . . . . 13
1402ad3antrrr 729 . . . . . . . . . . . . . . 15
14112ad3antrrr 729 . . . . . . . . . . . . . . 15
142 eldifi 3592 . . . . . . . . . . . . . . . 16
143142adantl 466 . . . . . . . . . . . . . . 15
1445, 10, 6, 140, 141, 143mvrcl 17705 . . . . . . . . . . . . . 14
145108, 86, 81mulg0 15791 . . . . . . . . . . . . . 14
146144, 145syl 16 . . . . . . . . . . . . 13
147139, 146eqtrd 2495 . . . . . . . . . . . 12
148147, 79suppss2 6857 . . . . . . . . . . 11
149 suppssfifsupp 7770 . . . . . . . . . . 11
150121, 123, 125, 126, 148, 149syl32anc 1227 . . . . . . . . . 10
15186, 91, 79, 94, 118, 150gsumsubmcl 16565 . . . . . . . . 9
15284, 151eqeltrd 2542 . . . . . . . 8
153 eqid 2454 . . . . . . . . 9
154 eqid 2454 . . . . . . . . 9
155153, 38, 154, 67lssvscl 17212 . . . . . . . 8
15663, 71, 78, 152, 155syl22anc 1220 . . . . . . 7
157 eqid 2454 . . . . . . 7
158156, 157fmptd 5990 . . . . . 6
15948mptrabex 6074 . . . . . . . . 9
160 funmpt 5573 . . . . . . . . 9
161 fvex 5823 . . . . . . . . 9
162159, 160, 1613pm3.2i 1166 . . . . . . . 8
163162a1i 11 . . . . . . 7
1645, 1, 7, 35, 6mplelbas 17681 . . . . . . . . . 10
165164simprbi 464 . . . . . . . . 9
166165adantl 466 . . . . . . . 8
167166fsuppimpd 7762 . . . . . . 7
168 ssid 3489 . . . . . . . . . . . . 13
169168a1i 11 . . . . . . . . . . . 12
170 fvex 5823 . . . . . . . . . . . . 13
171170a1i 11 . . . . . . . . . . . 12
17273, 169, 50, 171suppssr 6854 . . . . . . . . . . 11
17375fveq2d 5817 . . . . . . . . . . . 12
174173adantr 465 . . . . . . . . . . 11
175172, 174eqtrd 2495 . . . . . . . . . 10
176175oveq1d 6237 . . . . . . . . 9
177 eldifi 3592 . . . . . . . . . 10
17812ad2antrr 725 . . . . . . . . . . . 12
1795, 6, 35, 36, 34, 79, 178, 83mplmon 17719 . . . . . . . . . . 11
180 eqid 2454 . . . . . . . . . . . 12
1816, 153, 38, 180, 42lmod0vs 17157 . . . . . . . . . . 11
18263, 179, 181syl2anc 661 . . . . . . . . . 10
183177, 182sylan2 474 . . . . . . . . 9
184176, 183eqtrd 2495 . . . . . . . 8