Theorem ply1ring 22232

Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)

Hypothesis

Ref	Expression
ply1ring.p	⊢ 𝑃 = (Poly1‘𝑅)

Assertion

Ref	Expression
ply1ring	⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Proof of Theorem ply1ring

Step	Hyp	Ref	Expression
1		ply1ring.p	. . . 4 ⊢ 𝑃 = (Poly1‘𝑅)
2		eqid 2739	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22180	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2739	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22182	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2844	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22179	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20546	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ‘cfv 6485  (class class class)co 7356  1_oc1o 8388  Basecbs 17170  Ringcrg 20205  SubRingcsubrg 20541   mPoly cmpl 21881  PwSer₁cps1 22160  Poly₁cpl1 22162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-ofr 7621  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9265  df-sup 9345  df-oi 9415  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-fz 13453  df-fzo 13600  df-seq 13955  df-hash 14284  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-hom 17235  df-cco 17236  df-0g 17395  df-gsum 17396  df-prds 17401  df-pws 17403  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18742  df-submnd 18743  df-grp 18903  df-minusg 18904  df-mulg 19035  df-subg 19090  df-ghm 19179  df-cntz 19283  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-ring 20207  df-subrng 20518  df-subrg 20542  df-psr 21884  df-mpl 21886  df-opsr 21888  df-psr1 22165  df-ply1 22167

This theorem is referenced by:  ply1ascl0  22239  ply1ascl1  22240  coe1z  22249  coe1add  22250  coe1subfv  22252  ply1moncl  22257  coe1pwmul  22265  ply1sclf  22271  ply1scl0  22276  ply1scl1  22278  ply1coefsupp  22283  ply1coe  22284  cply1coe0bi  22288  coe1fzgsumdlem  22289  gsumsmonply1  22293  gsummoncoe1  22294  lply1binom  22296  lply1binomsc  22297  evls1sca  22309  evls1gsumadd  22310  evl1expd  22331  evl1gsumdlem  22342  evl1scvarpw  22349  evl1scvarpwval  22350  evl1gsummon  22351  evls1fpws  22355  evls1addd  22357  evls1muld  22358  rhmply1mon  22372  pmatring  22675  pmatlmod  22676  pmat0op  22678  pmat1op  22679  pmat1ovd  22680  1pmatscmul  22685  cpmatacl  22699  cpmatinvcl  22700  cpmatmcllem  22701  cpmatmcl  22702  mat2pmatbas  22709  mat2pmatghm  22713  mat2pmatmul  22714  mat2pmat1  22715  mat2pmatmhm  22716  mat2pmatrhm  22717  mat2pmatlin  22718  mat2pmatscmxcl  22723  m2pmfzgsumcl  22731  decpmatmullem  22754  pmatcollpw1  22759  pmatcollpw2lem  22760  pmatcollpw2  22761  monmatcollpw  22762  pmatcollpwlem  22763  pmatcollpw  22764  pmatcollpwfi  22765  pmatcollpw3fi1lem1  22769  pmatcollpwscmatlem1  22772  pmatcollpwscmatlem2  22773  pm2mpcl  22780  idpm2idmp  22784  mply1topmatcllem  22786  mply1topmatcl  22788  mp2pm2mplem2  22790  mp2pm2mplem4  22792  mp2pm2mp  22794  pm2mpghm  22799  pm2mpmhmlem2  22802  pm2mpmhm  22803  pm2mprhm  22804  monmat2matmon  22807  pm2mp  22808  chmatcl  22811  chmatval  22812  chpmat0d  22817  chpmat1dlem  22818  chpmat1d  22819  chpdmatlem0  22820  chpdmatlem2  22822  chpdmatlem3  22823  chpscmat  22825  chpscmatgsumbin  22827  chpscmatgsummon  22828  chp0mat  22829  chpidmat  22830  chmaidscmat  22831  chfacfscmulcl  22840  chfacfscmul0  22841  cpmadugsumlemB  22857  cpmadugsumlemC  22858  cpmadugsumlemF  22859  deg1addle2  26085  deg1add  26086  deg1suble  26090  deg1sub  26091  deg1sublt  26093  deg1mul2  26097  deg1mul3  26099  deg1mul3le  26100  deg1pw  26104  ply1nz  26105  ply1domn  26107  ply1divmo  26119  ply1divex  26120  uc1pmon1p  26135  r1pcl  26142  r1pid  26144  dvdsq1p  26146  dvdsr1p  26147  ply1remlem  26148  ply1rem  26149  idomrootle  26156  ig1peu  26158  ig1pval2  26160  ig1pdvds  26163  ig1prsp  26164  ply1lpir  26165  plypf1  26195  lgsqrlem2  27328  lgsqrlem3  27329  lgsqrlem4  27330  ressasclcl  33654  evls1subd  33655  ply1unit  33658  evls1monply1  33662  m1pmeq  33668  ply1coedeg  33672  ply1degltel  33677  ply1degleel  33678  ply1degltlss  33679  gsummoncoe1fzo  33680  ply1gsumz  33682  deg1addlt  33683  ig1pnunit  33684  q1pdir  33686  q1pvsca  33687  r1pvsca  33688  r1p0  33689  r1pcyc  33690  r1padd1  33691  r1pid2OLD  33692  r1plmhm  33693  r1pquslmic  33694  selvply1rhmlem4  33707  selvply1rhm  33709  vietadeg1  33762  ply1degltdimlem  33806  ply1degltdim  33807  extdgfialglem2  33877  ply1annnr  33887  irngnminplynz  33896  minplym1p  33897  minplynzm1p  33898  irredminply  33900  algextdeglem6  33906  algextdeglem8  33908  rtelextdg2lem  33910  2sqr3minply  33964  cos9thpiminplylem6  33971  cos9thpiminply  33972  ply1divalg3  35870  aks6d1c1p6  42599  aks6d1c6lem1  42655  aks6d1c6lem2  42656  hbtlem2  43569  hbtlem4  43571  hbtlem5  43573  hbtlem6  43574  hbt  43575  ply1sclrmsm  48875  ply1mulgsumlem4  48880  ply1mulgsum  48881  linply1  48884