Theorem ply1ring 22211

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  1_oc1o 8398  Basecbs 17179  Ringcrg 20214  SubRingcsubrg 20546   mPoly cmpl 21886  PwSer₁cps1 22138  Poly₁cpl1 22140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4851  df-int 4890  df-iun 4935  df-iin 4936  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-isom 6507  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-of 7631  df-ofr 7632  df-om 7818  df-1st 7942  df-2nd 7943  df-supp 8111  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-1o 8405  df-2o 8406  df-er 8643  df-map 8775  df-pm 8776  df-ixp 8846  df-en 8894  df-dom 8895  df-sdom 8896  df-fin 8897  df-fsupp 9275  df-sup 9355  df-oi 9425  df-card 9863  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249  df-8 12250  df-9 12251  df-n0 12438  df-z 12525  df-dec 12645  df-uz 12789  df-fz 13462  df-fzo 13609  df-seq 13964  df-hash 14293  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-mulr 17234  df-sca 17236  df-vsca 17237  df-ip 17238  df-tset 17239  df-ple 17240  df-ds 17242  df-hom 17244  df-cco 17245  df-0g 17404  df-gsum 17405  df-prds 17410  df-pws 17412  df-mre 17548  df-mrc 17549  df-acs 17551  df-mgm 18608  df-sgrp 18687  df-mnd 18703  df-mhm 18751  df-submnd 18752  df-grp 18912  df-minusg 18913  df-mulg 19044  df-subg 19099  df-ghm 19188  df-cntz 19292  df-cmn 19757  df-abl 19758  df-mgp 20122  df-rng 20134  df-ur 20163  df-ring 20216  df-subrng 20523  df-subrg 20547  df-psr 21889  df-mpl 21891  df-opsr 21893  df-psr1 22143  df-ply1 22145

This theorem is referenced by:  ply1ascl0  22218  ply1ascl1  22219  coe1z  22228  coe1add  22229  coe1subfv  22231  ply1moncl  22236  coe1pwmul  22244  ply1sclf  22250  ply1scl0  22255  ply1scl1  22257  ply1coefsupp  22262  ply1coe  22263  cply1coe0bi  22267  coe1fzgsumdlem  22268  gsumsmonply1  22272  gsummoncoe1  22273  lply1binom  22275  lply1binomsc  22276  evls1sca  22288  evls1gsumadd  22289  evl1expd  22310  evl1gsumdlem  22321  evl1scvarpw  22328  evl1scvarpwval  22329  evl1gsummon  22330  evls1fpws  22334  evls1addd  22336  evls1muld  22337  rhmply1mon  22354  pmatring  22657  pmatlmod  22658  pmat0op  22660  pmat1op  22661  pmat1ovd  22662  1pmatscmul  22667  cpmatacl  22681  cpmatinvcl  22682  cpmatmcllem  22683  cpmatmcl  22684  mat2pmatbas  22691  mat2pmatghm  22695  mat2pmatmul  22696  mat2pmat1  22697  mat2pmatmhm  22698  mat2pmatrhm  22699  mat2pmatlin  22700  mat2pmatscmxcl  22705  m2pmfzgsumcl  22713  decpmatmullem  22736  pmatcollpw1  22741  pmatcollpw2lem  22742  pmatcollpw2  22743  monmatcollpw  22744  pmatcollpwlem  22745  pmatcollpw  22746  pmatcollpwfi  22747  pmatcollpw3fi1lem1  22751  pmatcollpwscmatlem1  22754  pmatcollpwscmatlem2  22755  pm2mpcl  22762  idpm2idmp  22766  mply1topmatcllem  22768  mply1topmatcl  22770  mp2pm2mplem2  22772  mp2pm2mplem4  22774  mp2pm2mp  22776  pm2mpghm  22781  pm2mpmhmlem2  22784  pm2mpmhm  22785  pm2mprhm  22786  monmat2matmon  22789  pm2mp  22790  chmatcl  22793  chmatval  22794  chpmat0d  22799  chpmat1dlem  22800  chpmat1d  22801  chpdmatlem0  22802  chpdmatlem2  22804  chpdmatlem3  22805  chpscmat  22807  chpscmatgsumbin  22809  chpscmatgsummon  22810  chp0mat  22811  chpidmat  22812  chmaidscmat  22813  chfacfscmulcl  22822  chfacfscmul0  22823  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  deg1addle2  26067  deg1add  26068  deg1suble  26072  deg1sub  26073  deg1sublt  26075  deg1mul2  26079  deg1mul3  26081  deg1mul3le  26082  deg1pw  26086  ply1nz  26087  ply1domn  26089  ply1divmo  26101  ply1divex  26102  uc1pmon1p  26117  r1pcl  26124  r1pid  26126  dvdsq1p  26128  dvdsr1p  26129  ply1remlem  26130  ply1rem  26131  idomrootle  26138  ig1peu  26140  ig1pval2  26142  ig1pdvds  26145  ig1prsp  26146  ply1lpir  26147  plypf1  26177  lgsqrlem2  27310  lgsqrlem3  27311  lgsqrlem4  27312  ressasclcl  33631  evls1subd  33632  ply1unit  33635  evls1monply1  33639  m1pmeq  33645  ply1coedeg  33649  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  gsummoncoe1fzo  33657  ply1gsumz  33659  deg1addlt  33660  ig1pnunit  33661  q1pdir  33663  q1pvsca  33664  r1pvsca  33665  r1p0  33666  r1pcyc  33667  r1padd1  33668  r1pid2OLD  33669  r1plmhm  33670  r1pquslmic  33671  vietadeg1  33722  ply1degltdimlem  33766  ply1degltdim  33767  extdgfialglem2  33837  ply1annnr  33847  irngnminplynz  33856  minplym1p  33857  minplynzm1p  33858  irredminply  33860  algextdeglem6  33866  algextdeglem8  33868  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminplylem6  33931  cos9thpiminply  33932  ply1divalg3  35824  aks6d1c1p6  42553  aks6d1c6lem1  42609  aks6d1c6lem2  42610  hbtlem2  43552  hbtlem4  43554  hbtlem5  43556  hbtlem6  43557  hbt  43558  ply1sclrmsm  48860  ply1mulgsumlem4  48865  ply1mulgsum  48866  linply1  48869