Theorem ply1ring 20418

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 2823	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
3		eqid 2823	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
4	1, 2, 3	ply1bas 20365	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
5	1, 2, 3	ply1subrg 20367	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	4, 5	eqeltrrid 2920	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 2	ply1val 20364	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 19540	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  1_oc1o 8097  Basecbs 16485  Ringcrg 19299  SubRingcsubrg 19533   mPoly cmpl 20135  PwSer₁cps1 20345  Poly₁cpl1 20347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-rep 5192  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-iin 4924  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-se 5517  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-of 7411  df-ofr 7412  df-om 7583  df-1st 7691  df-2nd 7692  df-supp 7833  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-2o 8105  df-oadd 8108  df-er 8291  df-map 8410  df-pm 8411  df-ixp 8464  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-fsupp 8836  df-oi 8976  df-card 9370  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-fz 12896  df-fzo 13037  df-seq 13373  df-hash 13694  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-sets 16492  df-ress 16493  df-plusg 16580  df-mulr 16581  df-sca 16583  df-vsca 16584  df-tset 16586  df-ple 16587  df-0g 16717  df-gsum 16718  df-mre 16859  df-mrc 16860  df-acs 16862  df-mgm 17854  df-sgrp 17903  df-mnd 17914  df-mhm 17958  df-submnd 17959  df-grp 18108  df-minusg 18109  df-mulg 18227  df-subg 18278  df-ghm 18358  df-cntz 18449  df-cmn 18910  df-abl 18911  df-mgp 19242  df-ur 19254  df-ring 19301  df-subrg 19535  df-psr 20138  df-mpl 20140  df-opsr 20142  df-psr1 20350  df-ply1 20352

This theorem is referenced by:  coe1z  20433  coe1add  20434  coe1subfv  20436  ply1moncl  20441  coe1pwmul  20449  ply1sclf  20455  ply1scl0  20460  ply1scl1  20462  ply1coefsupp  20465  ply1coe  20466  cply1coe0bi  20470  coe1fzgsumdlem  20471  gsumsmonply1  20473  gsummoncoe1  20474  lply1binom  20476  lply1binomsc  20477  evls1sca  20488  evls1gsumadd  20489  evl1expd  20510  evl1gsumdlem  20521  evl1scvarpw  20528  evl1scvarpwval  20529  evl1gsummon  20530  pmatring  21303  pmatlmod  21304  pmat0op  21305  pmat1op  21306  pmat1ovd  21307  1pmatscmul  21312  cpmatacl  21326  cpmatinvcl  21327  cpmatmcllem  21328  cpmatmcl  21329  mat2pmatbas  21336  mat2pmatghm  21340  mat2pmatmul  21341  mat2pmat1  21342  mat2pmatmhm  21343  mat2pmatrhm  21344  mat2pmatlin  21345  mat2pmatscmxcl  21350  m2pmfzgsumcl  21358  decpmatmullem  21381  pmatcollpw1  21386  pmatcollpw2lem  21387  pmatcollpw2  21388  monmatcollpw  21389  pmatcollpwlem  21390  pmatcollpw  21391  pmatcollpwfi  21392  pmatcollpw3fi1lem1  21396  pmatcollpwscmatlem1  21399  pmatcollpwscmatlem2  21400  pm2mpcl  21407  idpm2idmp  21411  mply1topmatcllem  21413  mply1topmatcl  21415  mp2pm2mplem2  21417  mp2pm2mplem4  21419  mp2pm2mp  21421  pm2mpghm  21426  pm2mpmhmlem2  21429  pm2mpmhm  21430  pm2mprhm  21431  pm2mprngiso  21432  monmat2matmon  21434  pm2mp  21435  chmatcl  21438  chmatval  21439  chpmat0d  21444  chpmat1dlem  21445  chpmat1d  21446  chpdmatlem0  21447  chpdmatlem2  21449  chpdmatlem3  21450  chpscmat  21452  chpscmatgsumbin  21454  chpscmatgsummon  21455  chp0mat  21456  chpidmat  21457  chmaidscmat  21458  chfacfscmulcl  21467  chfacfscmul0  21468  cpmadugsumlemB  21484  cpmadugsumlemC  21485  cpmadugsumlemF  21486  deg1addle2  24698  deg1add  24699  deg1suble  24703  deg1sub  24704  deg1sublt  24706  deg1mul2  24710  deg1mul3  24711  deg1mul3le  24712  deg1pw  24716  ply1nz  24717  ply1domn  24719  ply1divmo  24731  ply1divex  24732  uc1pmon1p  24747  r1pcl  24753  r1pid  24755  dvdsq1p  24756  dvdsr1p  24757  ply1remlem  24758  ply1rem  24759  ig1peu  24767  ig1pval2  24769  ig1pdvds  24772  ig1prsp  24773  ply1lpir  24774  plypf1  24804  lgsqrlem2  25925  lgsqrlem3  25926  lgsqrlem4  25927  hbtlem2  39731  hbtlem4  39733  hbtlem5  39735  hbtlem6  39736  hbt  39737  idomrootle  39802  ply1sclrmsm  44444  ply1mulgsumlem4  44450  ply1mulgsum  44451  linply1  44454