Theorem ply1ring 22216

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 2734	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22163	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2734	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22166	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2838	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22162	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20547	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ‘cfv 6542  (class class class)co 7414  1_oc1o 8482  Basecbs 17230  Ringcrg 20203  SubRingcsubrg 20542   mPoly cmpl 21893  PwSer₁cps1 22143  Poly₁cpl1 22145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5261  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-pss 3953  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-tp 4613  df-op 4615  df-uni 4890  df-int 4929  df-iun 4975  df-iin 4976  df-br 5126  df-opab 5188  df-mpt 5208  df-tr 5242  df-id 5560  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-se 5620  df-we 5621  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6303  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7680  df-ofr 7681  df-om 7871  df-1st 7997  df-2nd 7998  df-supp 8169  df-frecs 8289  df-wrecs 8320  df-recs 8394  df-rdg 8433  df-1o 8489  df-2o 8490  df-er 8728  df-map 8851  df-pm 8852  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9385  df-sup 9465  df-oi 9533  df-card 9962  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11477  df-neg 11478  df-nn 12250  df-2 12312  df-3 12313  df-4 12314  df-5 12315  df-6 12316  df-7 12317  df-8 12318  df-9 12319  df-n0 12511  df-z 12598  df-dec 12718  df-uz 12862  df-fz 13531  df-fzo 13678  df-seq 14026  df-hash 14353  df-struct 17167  df-sets 17184  df-slot 17202  df-ndx 17214  df-base 17231  df-ress 17257  df-plusg 17290  df-mulr 17291  df-sca 17293  df-vsca 17294  df-ip 17295  df-tset 17296  df-ple 17297  df-ds 17299  df-hom 17301  df-cco 17302  df-0g 17462  df-gsum 17463  df-prds 17468  df-pws 17470  df-mre 17605  df-mrc 17606  df-acs 17608  df-mgm 18627  df-sgrp 18706  df-mnd 18722  df-mhm 18770  df-submnd 18771  df-grp 18928  df-minusg 18929  df-mulg 19060  df-subg 19115  df-ghm 19205  df-cntz 19309  df-cmn 19773  df-abl 19774  df-mgp 20111  df-rng 20123  df-ur 20152  df-ring 20205  df-subrng 20519  df-subrg 20543  df-psr 21896  df-mpl 21898  df-opsr 21900  df-psr1 22148  df-ply1 22150

This theorem is referenced by:  ply1ascl0  22223  ply1ascl1  22224  coe1z  22233  coe1add  22234  coe1subfv  22236  ply1moncl  22241  coe1pwmul  22249  ply1sclf  22255  ply1scl0  22260  ply1scl0OLD  22261  ply1scl1  22263  ply1scl1OLD  22264  ply1coefsupp  22268  ply1coe  22269  cply1coe0bi  22273  coe1fzgsumdlem  22274  gsumsmonply1  22278  gsummoncoe1  22279  lply1binom  22281  lply1binomsc  22282  evls1sca  22294  evls1gsumadd  22295  evl1expd  22316  evl1gsumdlem  22327  evl1scvarpw  22334  evl1scvarpwval  22335  evl1gsummon  22336  evls1fpws  22340  evls1addd  22342  evls1muld  22343  rhmply1mon  22360  pmatring  22665  pmatlmod  22666  pmat0op  22668  pmat1op  22669  pmat1ovd  22670  1pmatscmul  22675  cpmatacl  22689  cpmatinvcl  22690  cpmatmcllem  22691  cpmatmcl  22692  mat2pmatbas  22699  mat2pmatghm  22703  mat2pmatmul  22704  mat2pmat1  22705  mat2pmatmhm  22706  mat2pmatrhm  22707  mat2pmatlin  22708  mat2pmatscmxcl  22713  m2pmfzgsumcl  22721  decpmatmullem  22744  pmatcollpw1  22749  pmatcollpw2lem  22750  pmatcollpw2  22751  monmatcollpw  22752  pmatcollpwlem  22753  pmatcollpw  22754  pmatcollpwfi  22755  pmatcollpw3fi1lem1  22759  pmatcollpwscmatlem1  22762  pmatcollpwscmatlem2  22763  pm2mpcl  22770  idpm2idmp  22774  mply1topmatcllem  22776  mply1topmatcl  22778  mp2pm2mplem2  22780  mp2pm2mplem4  22782  mp2pm2mp  22784  pm2mpghm  22789  pm2mpmhmlem2  22792  pm2mpmhm  22793  pm2mprhm  22794  monmat2matmon  22797  pm2mp  22798  chmatcl  22801  chmatval  22802  chpmat0d  22807  chpmat1dlem  22808  chpmat1d  22809  chpdmatlem0  22810  chpdmatlem2  22812  chpdmatlem3  22813  chpscmat  22815  chpscmatgsumbin  22817  chpscmatgsummon  22818  chp0mat  22819  chpidmat  22820  chmaidscmat  22821  chfacfscmulcl  22830  chfacfscmul0  22831  cpmadugsumlemB  22847  cpmadugsumlemC  22848  cpmadugsumlemF  22849  deg1addle2  26096  deg1add  26097  deg1suble  26101  deg1sub  26102  deg1sublt  26104  deg1mul2  26108  deg1mul3  26110  deg1mul3le  26111  deg1pw  26115  ply1nz  26116  ply1domn  26118  ply1divmo  26130  ply1divex  26131  uc1pmon1p  26146  r1pcl  26153  r1pid  26155  dvdsq1p  26157  dvdsr1p  26158  ply1remlem  26159  ply1rem  26160  idomrootle  26167  ig1peu  26169  ig1pval2  26171  ig1pdvds  26174  ig1prsp  26175  ply1lpir  26176  plypf1  26206  lgsqrlem2  27346  lgsqrlem3  27347  lgsqrlem4  27348  ressasclcl  33537  evls1subd  33538  ply1unit  33541  m1pmeq  33549  ply1degltel  33556  ply1degleel  33557  ply1degltlss  33558  gsummoncoe1fzo  33559  ply1gsumz  33560  deg1addlt  33561  ig1pnunit  33562  q1pdir  33564  q1pvsca  33565  r1pvsca  33566  r1p0  33567  r1pcyc  33568  r1padd1  33569  r1pid2OLD  33570  r1plmhm  33571  r1pquslmic  33572  ply1degltdimlem  33614  ply1degltdim  33615  ply1annnr  33687  irngnminplynz  33696  minplym1p  33697  irredminply  33698  algextdeglem6  33704  algextdeglem8  33706  rtelextdg2lem  33708  2sqr3minply  33732  ply1divalg3  35588  aks6d1c1p6  42056  aks6d1c6lem1  42112  aks6d1c6lem2  42113  hbtlem2  43081  hbtlem4  43083  hbtlem5  43085  hbtlem6  43086  hbt  43087  ply1sclrmsm  48246  ply1mulgsumlem4  48252  ply1mulgsum  48253  linply1  48256