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

Theorem ply1rng 18100
Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
Hypothesis
Ref Expression
ply1rng.p  |-  P  =  (Poly1 `  R )
Assertion
Ref Expression
ply1rng  |-  ( R  e.  Ring  ->  P  e. 
Ring )

Proof of Theorem ply1rng
StepHypRef Expression
1 ply1rng.p . . . 4  |-  P  =  (Poly1 `  R )
2 eqid 2467 . . . 4  |-  (PwSer1 `  R
)  =  (PwSer1 `  R
)
3 eqid 2467 . . . 4  |-  ( Base `  P )  =  (
Base `  P )
41, 2, 3ply1bas 18045 . . 3  |-  ( Base `  P )  =  (
Base `  ( 1o mPoly  R ) )
51, 2, 3ply1subrg 18047 . . 3  |-  ( R  e.  Ring  ->  ( Base `  P )  e.  (SubRing `  (PwSer1 `  R ) ) )
64, 5syl5eqelr 2560 . 2  |-  ( R  e.  Ring  ->  ( Base `  ( 1o mPoly  R )
)  e.  (SubRing `  (PwSer1 `  R ) ) )
71, 2ply1val 18044 . . 3  |-  P  =  ( (PwSer1 `  R )s  ( Base `  ( 1o mPoly  R )
) )
87subrgrng 17244 . 2  |-  ( (
Base `  ( 1o mPoly  R ) )  e.  (SubRing `  (PwSer1 `  R ) )  ->  P  e.  Ring )
96, 8syl 16 1  |-  ( R  e.  Ring  ->  P  e. 
Ring )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   ` cfv 5588  (class class class)co 6285   1oc1o 7124   Basecbs 14493   Ringcrg 17012  SubRingcsubrg 17237   mPoly cmpl 17813  PwSer1cps1 18025  Poly1cpl1 18027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6577  ax-inf2 8059  ax-cnex 9549  ax-resscn 9550  ax-1cn 9551  ax-icn 9552  ax-addcl 9553  ax-addrcl 9554  ax-mulcl 9555  ax-mulrcl 9556  ax-mulcom 9557  ax-addass 9558  ax-mulass 9559  ax-distr 9560  ax-i2m1 9561  ax-1ne0 9562  ax-1rid 9563  ax-rnegex 9564  ax-rrecex 9565  ax-cnre 9566  ax-pre-lttri 9567  ax-pre-lttrn 9568  ax-pre-ltadd 9569  ax-pre-mulgt0 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6246  df-ov 6288  df-oprab 6289  df-mpt2 6290  df-of 6525  df-ofr 6526  df-om 6686  df-1st 6785  df-2nd 6786  df-supp 6903  df-recs 7043  df-rdg 7077  df-1o 7131  df-2o 7132  df-oadd 7135  df-er 7312  df-map 7423  df-pm 7424  df-ixp 7471  df-en 7518  df-dom 7519  df-sdom 7520  df-fin 7521  df-fsupp 7831  df-oi 7936  df-card 8321  df-pnf 9631  df-mnf 9632  df-xr 9633  df-ltxr 9634  df-le 9635  df-sub 9808  df-neg 9809  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-uz 11084  df-fz 11674  df-fzo 11794  df-seq 12077  df-hash 12375  df-struct 14495  df-ndx 14496  df-slot 14497  df-base 14498  df-sets 14499  df-ress 14500  df-plusg 14571  df-mulr 14572  df-sca 14574  df-vsca 14575  df-tset 14577  df-ple 14578  df-0g 14700  df-gsum 14701  df-mre 14844  df-mrc 14845  df-acs 14847  df-mnd 15735  df-mhm 15789  df-submnd 15790  df-grp 15871  df-minusg 15872  df-mulg 15874  df-subg 16012  df-ghm 16079  df-cntz 16169  df-cmn 16615  df-abl 16616  df-mgp 16956  df-ur 16968  df-rng 17014  df-subrg 17239  df-psr 17816  df-mpl 17818  df-opsr 17820  df-psr1 18030  df-ply1 18032
This theorem is referenced by:  coe1z  18115  coe1add  18116  coe1subfv  18118  ply1moncl  18123  coe1pwmul  18131  ply1sclf  18137  ply1scl0  18142  ply1scl1  18144  ply1coefsupp  18147  ply1coe  18148  cply1coe0bi  18153  coe1fzgsumdlem  18154  gsumsmonply1  18156  gsummoncoe1  18157  lply1binom  18159  lply1binomsc  18160  evls1sca  18171  evls1gsumadd  18172  evl1expd  18192  evl1gsumdlem  18203  evl1scvarpw  18210  evl1scvarpwval  18211  evl1gsummon  18212  pmatrng  19001  pmatlmod  19002  pmat0op  19003  pmat1op  19004  pmat1ovd  19005  1pmatscmul  19010  cpmatacl  19024  cpmatinvcl  19025  cpmatmcllem  19026  cpmatmcl  19027  cpmatsubgpmat  19028  cpmatsrgpmat  19029  mat2pmatbas  19034  mat2pmatghm  19038  mat2pmatmul  19039  mat2pmat1  19040  mat2pmatmhm  19041  mat2pmatrhm  19042  mat2pmatlin  19043  mat2pmatscmxcl  19048  m2pmfzgsumcl  19056  decpmatmullem  19079  pmatcollpw1  19084  pmatcollpw2lem  19085  pmatcollpw2  19086  monmatcollpw  19087  pmatcollpwlem  19088  pmatcollpw  19089  pmatcollpwfi  19090  pmatcollpw3fi1lem1  19094  pmatcollpwscmatlem1  19097  pmatcollpwscmatlem2  19098  pm2mpcl  19105  idpm2idmp  19109  mply1topmatcllem  19111  mply1topmatcl  19113  mp2pm2mplem2  19115  mp2pm2mplem4  19117  mp2pm2mp  19119  pm2mpghm  19124  pm2mpmhmlem2  19127  pm2mpmhm  19128  pm2mprhm  19129  pm2mprngiso  19130  monmat2matmon  19132  pm2mp  19133  chmatcl  19136  chmatval  19137  chpmat0d  19142  chpmat1dlem  19143  chpmat1d  19144  chpdmatlem0  19145  chpdmatlem1  19146  chpdmatlem2  19147  chpdmatlem3  19148  chpscmat  19150  chpscmatgsumbin  19152  chpscmatgsummon  19153  chp0mat  19154  chpidmat  19155  chmaidscmat  19156  chfacfscmulcl  19165  chfacfscmul0  19166  cpmadugsumlemB  19182  cpmadugsumlemC  19183  cpmadugsumlemF  19184  deg1addle2  22330  deg1add  22331  deg1suble  22335  deg1sub  22336  deg1sublt  22338  deg1mul2  22342  deg1mul3  22343  deg1mul3le  22344  deg1pwle  22347  deg1pw  22348  ply1nz  22349  ply1domn  22351  ply1divmo  22363  ply1divex  22364  uc1pmon1p  22379  r1pcl  22385  r1pid  22387  dvdsq1p  22388  dvdsr1p  22389  ply1remlem  22390  ply1rem  22391  ig1peu  22399  ig1pval2  22401  ig1pdvds  22404  ig1prsp  22405  ply1lpir  22406  plypf1  22436  lgsqrlem2  23442  lgsqrlem3  23443  lgsqrlem4  23444  hbtlem2  30904  hbtlem4  30906  hbtlem5  30908  hbtlem6  30909  hbt  30910  idomrootle  30984  ply1sclrmsm  32281  ply1mulgsumlem4  32287  ply1mulgsum  32288  linply1  32291
  Copyright terms: Public domain W3C validator