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

Theorem mplbas2 17354
 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 17297 . . . 4
5 mplbas2.p . . . . . 6
6 eqid 2422 . . . . . 6
7 eqid 2422 . . . . . 6
85, 1, 6, 7mplbasss 17319 . . . . 5
98a1i 11 . . . 4
10 mplbas2.v . . . . . . . 8
11 crngrng 16483 . . . . . . . . 9
123, 11syl 16 . . . . . . . 8
131, 10, 7, 2, 12mvrf 17308 . . . . . . 7
14 ffn 5529 . . . . . . 7
1513, 14syl 16 . . . . . 6
162adantr 455 . . . . . . . 8
1712adantr 455 . . . . . . . 8
18 simpr 451 . . . . . . . 8
195, 10, 6, 16, 17, 18mvrcl 17335 . . . . . . 7
2019ralrimiva 2778 . . . . . 6
21 ffnfv 5838 . . . . . 6
2215, 20, 21sylanbrc 649 . . . . 5
23 frn 5535 . . . . 5
2422, 23syl 16 . . . 4
25 mplbas2.a . . . . 5
2625, 7aspss 17211 . . . 4
274, 9, 24, 26syl3anc 1203 . . 3
281, 5, 6, 2, 12mplsubrg 17326 . . . 4
291, 5, 6, 2, 12mpllss 17324 . . . 4
30 eqid 2422 . . . . 5
3125, 7, 30aspid 17209 . . . 4
324, 28, 29, 31syl3anc 1203 . . 3
3327, 32sseqtrd 3369 . 2
34 eqid 2422 . . . . . 6
35 eqid 2422 . . . . . 6
36 eqid 2422 . . . . . 6
372adantr 455 . . . . . 6
38 eqid 2422 . . . . . 6
3912adantr 455 . . . . . 6
40 simpr 451 . . . . . 6
415, 34, 35, 36, 37, 6, 38, 39, 40mplcoe1 17351 . . . . 5
42 eqid 2422 . . . . . 6
435mplrng 17338 . . . . . . . . 9
442, 12, 43syl2anc 646 . . . . . . . 8
45 rngabl 16502 . . . . . . . 8
4644, 45syl 16 . . . . . . 7
4746adantr 455 . . . . . 6
48 ovex 6086 . . . . . . . 8
4948rabex 4418 . . . . . . 7
5049a1i 11 . . . . . 6
5124, 8syl6ss 3345 . . . . . . . . . 10
5225, 7aspsubrg 17210 . . . . . . . . . 10
534, 51, 52syl2anc 646 . . . . . . . . 9
545, 1, 6mplval2 17318 . . . . . . . . . . 11
5554subsubrg 16704 . . . . . . . . . 10
5628, 55syl 16 . . . . . . . . 9
5753, 33, 56mpbir2and 898 . . . . . . . 8
58 subrgsubg 16684 . . . . . . . 8
5957, 58syl 16 . . . . . . 7
6059adantr 455 . . . . . 6
615mpllmod 17337 . . . . . . . . . 10
622, 12, 61syl2anc 646 . . . . . . . . 9
6362ad2antrr 710 . . . . . . . 8
6425, 7, 30asplss 17208 . . . . . . . . . . 11
654, 51, 64syl2anc 646 . . . . . . . . . 10
661, 2, 12psrlmod 17285 . . . . . . . . . . 11
67 eqid 2422 . . . . . . . . . . . 12
6854, 30, 67lsslss 16851 . . . . . . . . . . 11
6966, 29, 68syl2anc 646 . . . . . . . . . 10
7065, 33, 69mpbir2and 898 . . . . . . . . 9
7170ad2antrr 710 . . . . . . . 8
72 eqid 2422 . . . . . . . . . . 11
735, 72, 6, 34, 40mplelf 17320 . . . . . . . . . 10
7473ffvelrnda 5813 . . . . . . . . 9
755, 37, 39mplsca 17331 . . . . . . . . . . 11
7675adantr 455 . . . . . . . . . 10
7776fveq2d 5665 . . . . . . . . 9
7874, 77eleqtrd 2498 . . . . . . . 8
7937adantr 455 . . . . . . . . . 10
80 eqid 2422 . . . . . . . . . 10
81 eqid 2422 . . . . . . . . . 10
823adantr 455 . . . . . . . . . . 11
8382adantr 455 . . . . . . . . . 10
84 simpr 451 . . . . . . . . . 10
855, 34, 35, 36, 79, 80, 81, 10, 83, 84mplcoe2 17353 . . . . . . . . 9
86 eqid 2422 . . . . . . . . . . 11
8780, 86rngidval 16475 . . . . . . . . . 10
885mplcrng 17339 . . . . . . . . . . . . 13
892, 3, 88syl2anc 646 . . . . . . . . . . . 12
9080crngmgp 16481 . . . . . . . . . . . 12
9189, 90syl 16 . . . . . . . . . . 11
9291ad2antrr 710 . . . . . . . . . 10
9357ad2antrr 710 . . . . . . . . . . 11
9480subrgsubm 16691 . . . . . . . . . . 11
9593, 94syl 16 . . . . . . . . . 10
96 simplll 742 . . . . . . . . . . . 12
9734psrbag 17251 . . . . . . . . . . . . . . . 16
9837, 97syl 16 . . . . . . . . . . . . . . 15
9998biimpa 474 . . . . . . . . . . . . . 14
10099simpld 449 . . . . . . . . . . . . 13
101100ffvelrnda 5813 . . . . . . . . . . . 12
10225, 7aspssid 17212 . . . . . . . . . . . . . . 15
1034, 51, 102syl2anc 646 . . . . . . . . . . . . . 14
104103ad3antrrr 714 . . . . . . . . . . . . 13
10515ad2antrr 710 . . . . . . . . . . . . . 14
106 fnfvelrn 5810 . . . . . . . . . . . . . 14
107105, 106sylan 461 . . . . . . . . . . . . 13
108104, 107sseldd 3334 . . . . . . . . . . . 12
10980, 6mgpbas 16463 . . . . . . . . . . . . 13
110 eqid 2422 . . . . . . . . . . . . . 14
11180, 110mgpplusg 16461 . . . . . . . . . . . . 13
112110subrgmcl 16690 . . . . . . . . . . . . . 14
11357, 112syl3an1 1236 . . . . . . . . . . . . 13
11486subrg1cl 16686 . . . . . . . . . . . . . 14
11557, 114syl 16 . . . . . . . . . . . . 13
116109, 81, 111, 91, 33, 113, 87, 115mulgnn0subcl 15577 . . . . . . . . . . . 12
11796, 101, 108, 116syl3anc 1203 . . . . . . . . . . 11
118 eqid 2422 . . . . . . . . . . 11
119117, 118fmptd 5837 . . . . . . . . . 10
12099simprd 453 . . . . . . . . . . 11
121 nn0supp 10580 . . . . . . . . . . . . . . . 16
122 eqimss 3385 . . . . . . . . . . . . . . . 16
123100, 121, 1223syl 19 . . . . . . . . . . . . . . 15
124100, 123suppssrOLD 5807 . . . . . . . . . . . . . 14
125124oveq1d 6076 . . . . . . . . . . . . 13
12679adantr 455 . . . . . . . . . . . . . . 15
12739adantr 455 . . . . . . . . . . . . . . . 16
128127adantr 455 . . . . . . . . . . . . . . 15
129 eldifi 3455 . . . . . . . . . . . . . . . 16
130129adantl 456 . . . . . . . . . . . . . . 15
1315, 10, 6, 126, 128, 130mvrcl 17335 . . . . . . . . . . . . . 14
132109, 87, 81mulg0 15569 . . . . . . . . . . . . . 14
133131, 132syl 16 . . . . . . . . . . . . 13
134125, 133eqtrd 2454 . . . . . . . . . . . 12
135134suppss2OLD 6285 . . . . . . . . . . 11
136 ssfi 7492 . . . . . . . . . . 11
137120, 135, 136syl2anc 646 . . . . . . . . . 10
13887, 92, 79, 95, 119, 137gsumsubmcl 16327 . . . . . . . . 9
13985, 138eqeltrd 2496 . . . . . . . 8
140 eqid 2422 . . . . . . . . 9
141 eqid 2422 . . . . . . . . 9
142140, 38, 141, 67lssvscl 16845 . . . . . . . 8
14363, 71, 78, 139, 142syl22anc 1204 . . . . . . 7
144 eqid 2422 . . . . . . 7
145143, 144fmptd 5837 . . . . . 6
1465, 1, 7, 35, 6mplelbasOLD 17317 . . . . . . . . 9
147146simprbi 454 . . . . . . . 8
148147adantl 456 . . . . . . 7
149 ssid 3352 . . . . . . . . . . . . 13
150149a1i 11 . . . . . . . . . . . 12
15173, 150suppssrOLD 5807 . . . . . . . . . . 11
15275fveq2d 5665 . . . . . . . . . . . 12
153152adantr 455 . . . . . . . . . . 11
154151, 153eqtrd 2454 . . . . . . . . . 10
155154oveq1d 6076 . . . . . . . . 9
156 eldifi 3455 . . . . . . . . . 10
1575, 6, 35, 36, 34, 79, 127, 84mplmon 17349 . . . . . . . . . . 11
158 eqid 2422 . . . . . . . . . . . 12
1596, 140, 38, 158, 42lmod0vs 16794 . . . . . . . . . . 11
16063, 157, 159syl2anc 646 . . . . . . . . . 10
161156, 160sylan2 464 . . . . . . . . 9
162155, 161eqtrd 2454 . . . . . . . 8
163162suppss2OLD 6285 . . . . . . 7
164 ssfi 7492 . . . . . . 7
165148, 163, 164syl2anc 646 . . . . . 6
16642, 47, 50, 60, 145, 165gsumsubgcl 16328 . . . . 5
16741, 166eqeltrd 2496 . . . 4
168167ex 427 . . 3
169168ssrdv 3339 . 2
17033, 169eqssd 3350 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 178  /\wa 362  =wceq 1687  e.wcel 1749  A.wral 2694  {crab 2698   cvv 2951  \cdif 3302  C_wss 3305  ifcif 3768  {csn 3853  e.cmpt 4325  'ccnv 4810  rancrn 4812  "cima 4814  Fnwfn 5385  -->wf 5386  cfv 5390  (class class class)co 6061   cmap 7175   cfn 7269  0cc0 9228   cn 10268   cn0 10525   cbs 14114   cmulr 14179   csca 14181   cvsca 14182   c0g 14318   cgsu 14319   cmg 15354   csubmnd 15403   csubg 15612   ccmn 16214   cabel 16215   cmgp 16457   crg 16469   ccrg 16470   cur 16471   csubrg 16674   clmod 16761   clss 16822   casa 17189   casp 17190   cmps 17226   cmvr 17227   cmpl 17228 This theorem is referenced by:  mplind  17386  evlseu  21225 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-inf2 7794  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305 This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-int 4104  df-iun 4148  df-iin 4149  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-se 4651  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-isom 5399  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-of 6290  df-ofr 6291  df-om 6447  df-1st 6546  df-2nd 6547  df-supp 6660  df-recs 6791  df-rdg 6825  df-1o 6881  df-2o 6882  df-oadd 6885  df-er 7062  df-map 7177  df-pm 7178  df-ixp 7223  df-en 7270  df-dom 7271  df-sdom 7272  df-fin 7273  df-fsupp 7580  df-oi 7671  df-card 8056  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-nn 10269  df-2 10326  df-3 10327  df-4 10328  df-5 10329  df-6 10330  df-7 10331  df-8 10332  df-9 10333  df-n0 10526  df-z