Theorem ply1ring 22190

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 2736	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22137	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2736	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22140	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2841	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22136	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20509	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6492  (class class class)co 7358  1_oc1o 8390  Basecbs 17138  Ringcrg 20170  SubRingcsubrg 20504   mPoly cmpl 21864  PwSer₁cps1 22117  Poly₁cpl1 22119

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-rep 5224  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-tp 4585  df-op 4587  df-uni 4864  df-int 4903  df-iun 4948  df-iin 4949  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-isom 6501  df-riota 7315  df-ov 7361  df-oprab 7362  df-mpo 7363  df-of 7622  df-ofr 7623  df-om 7809  df-1st 7933  df-2nd 7934  df-supp 8103  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-rdg 8341  df-1o 8397  df-2o 8398  df-er 8635  df-map 8767  df-pm 8768  df-ixp 8838  df-en 8886  df-dom 8887  df-sdom 8888  df-fin 8889  df-fsupp 9267  df-sup 9347  df-oi 9417  df-card 9853  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-nn 12148  df-2 12210  df-3 12211  df-4 12212  df-5 12213  df-6 12214  df-7 12215  df-8 12216  df-9 12217  df-n0 12404  df-z 12491  df-dec 12610  df-uz 12754  df-fz 13426  df-fzo 13573  df-seq 13927  df-hash 14256  df-struct 17076  df-sets 17093  df-slot 17111  df-ndx 17123  df-base 17139  df-ress 17160  df-plusg 17192  df-mulr 17193  df-sca 17195  df-vsca 17196  df-ip 17197  df-tset 17198  df-ple 17199  df-ds 17201  df-hom 17203  df-cco 17204  df-0g 17363  df-gsum 17364  df-prds 17369  df-pws 17371  df-mre 17507  df-mrc 17508  df-acs 17510  df-mgm 18567  df-sgrp 18646  df-mnd 18662  df-mhm 18710  df-submnd 18711  df-grp 18868  df-minusg 18869  df-mulg 19000  df-subg 19055  df-ghm 19144  df-cntz 19248  df-cmn 19713  df-abl 19714  df-mgp 20078  df-rng 20090  df-ur 20119  df-ring 20172  df-subrng 20481  df-subrg 20505  df-psr 21867  df-mpl 21869  df-opsr 21871  df-psr1 22122  df-ply1 22124

This theorem is referenced by:  ply1ascl0  22197  ply1ascl1  22198  coe1z  22207  coe1add  22208  coe1subfv  22210  ply1moncl  22215  coe1pwmul  22223  ply1sclf  22229  ply1scl0  22234  ply1scl0OLD  22235  ply1scl1  22237  ply1scl1OLD  22238  ply1coefsupp  22243  ply1coe  22244  cply1coe0bi  22248  coe1fzgsumdlem  22249  gsumsmonply1  22253  gsummoncoe1  22254  lply1binom  22256  lply1binomsc  22257  evls1sca  22269  evls1gsumadd  22270  evl1expd  22291  evl1gsumdlem  22302  evl1scvarpw  22309  evl1scvarpwval  22310  evl1gsummon  22311  evls1fpws  22315  evls1addd  22317  evls1muld  22318  rhmply1mon  22335  pmatring  22638  pmatlmod  22639  pmat0op  22641  pmat1op  22642  pmat1ovd  22643  1pmatscmul  22648  cpmatacl  22662  cpmatinvcl  22663  cpmatmcllem  22664  cpmatmcl  22665  mat2pmatbas  22672  mat2pmatghm  22676  mat2pmatmul  22677  mat2pmat1  22678  mat2pmatmhm  22679  mat2pmatrhm  22680  mat2pmatlin  22681  mat2pmatscmxcl  22686  m2pmfzgsumcl  22694  decpmatmullem  22717  pmatcollpw1  22722  pmatcollpw2lem  22723  pmatcollpw2  22724  monmatcollpw  22725  pmatcollpwlem  22726  pmatcollpw  22727  pmatcollpwfi  22728  pmatcollpw3fi1lem1  22732  pmatcollpwscmatlem1  22735  pmatcollpwscmatlem2  22736  pm2mpcl  22743  idpm2idmp  22747  mply1topmatcllem  22749  mply1topmatcl  22751  mp2pm2mplem2  22753  mp2pm2mplem4  22755  mp2pm2mp  22757  pm2mpghm  22762  pm2mpmhmlem2  22765  pm2mpmhm  22766  pm2mprhm  22767  monmat2matmon  22770  pm2mp  22771  chmatcl  22774  chmatval  22775  chpmat0d  22780  chpmat1dlem  22781  chpmat1d  22782  chpdmatlem0  22783  chpdmatlem2  22785  chpdmatlem3  22786  chpscmat  22788  chpscmatgsumbin  22790  chpscmatgsummon  22791  chp0mat  22792  chpidmat  22793  chmaidscmat  22794  chfacfscmulcl  22803  chfacfscmul0  22804  cpmadugsumlemB  22820  cpmadugsumlemC  22821  cpmadugsumlemF  22822  deg1addle2  26065  deg1add  26066  deg1suble  26070  deg1sub  26071  deg1sublt  26073  deg1mul2  26077  deg1mul3  26079  deg1mul3le  26080  deg1pw  26084  ply1nz  26085  ply1domn  26087  ply1divmo  26099  ply1divex  26100  uc1pmon1p  26115  r1pcl  26122  r1pid  26124  dvdsq1p  26126  dvdsr1p  26127  ply1remlem  26128  ply1rem  26129  idomrootle  26136  ig1peu  26138  ig1pval2  26140  ig1pdvds  26143  ig1prsp  26144  ply1lpir  26145  plypf1  26175  lgsqrlem2  27316  lgsqrlem3  27317  lgsqrlem4  27318  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  vietadeg1  33736  ply1degltdimlem  33781  ply1degltdim  33782  extdgfialglem2  33852  ply1annnr  33862  irngnminplynz  33871  minplym1p  33872  minplynzm1p  33873  irredminply  33875  algextdeglem6  33881  algextdeglem8  33883  rtelextdg2lem  33885  2sqr3minply  33939  cos9thpiminplylem6  33946  cos9thpiminply  33947  ply1divalg3  35838  aks6d1c1p6  42390  aks6d1c6lem1  42446  aks6d1c6lem2  42447  hbtlem2  43387  hbtlem4  43389  hbtlem5  43391  hbtlem6  43392  hbt  43393  ply1sclrmsm  48651  ply1mulgsumlem4  48656  ply1mulgsum  48657  linply1  48660