Theorem ply1ring 22309

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 2762	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22257	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2762	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22259	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2867	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22256	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20624	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ‘cfv 6521  (class class class)co 7396  1_oc1o 8430  Basecbs 17245  Ringcrg 20283  SubRingcsubrg 20619   mPoly cmpl 21958  PwSer₁cps1 22237  Poly₁cpl1 22239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5227  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-mulcom 11137  ax-addass 11138  ax-mulass 11139  ax-distr 11140  ax-i2m1 11141  ax-1ne0 11142  ax-1rid 11143  ax-rnegex 11144  ax-rrecex 11145  ax-cnre 11146  ax-pre-lttri 11147  ax-pre-lttrn 11148  ax-pre-ltadd 11149  ax-pre-mulgt0 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1099  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3456  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-tp 4587  df-op 4589  df-uni 4866  df-int 4906  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6288  df-ord 6349  df-on 6350  df-lim 6351  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-isom 6530  df-riota 7353  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7660  df-ofr 7661  df-om 7847  df-1st 7970  df-2nd 7971  df-supp 8141  df-frecs 8262  df-wrecs 8293  df-recs 8342  df-rdg 8381  df-1o 8437  df-2o 8438  df-er 8678  df-map 8810  df-pm 8811  df-ixp 8880  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fsupp 9308  df-sup 9388  df-oi 9458  df-card 9897  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222  df-sub 11416  df-neg 11417  df-nn 12211  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12482  df-z 12569  df-dec 12689  df-uz 12840  df-fz 13513  df-fzo 13660  df-seq 14015  df-hash 14344  df-struct 17183  df-sets 17200  df-slot 17218  df-ndx 17230  df-base 17246  df-ress 17267  df-plusg 17299  df-mulr 17300  df-sca 17302  df-vsca 17303  df-ip 17304  df-tset 17305  df-ple 17306  df-ds 17308  df-hom 17310  df-cco 17311  df-0g 17470  df-gsum 17471  df-prds 17476  df-pws 17478  df-mre 17614  df-mrc 17615  df-acs 17617  df-mgm 18674  df-sgrp 18753  df-mnd 18769  df-mhm 18817  df-submnd 18818  df-grp 18978  df-minusg 18979  df-mulg 19110  df-subg 19165  df-ghm 19254  df-cntz 19357  df-cmn 19822  df-abl 19823  df-mgp 20187  df-rng 20199  df-ur 20232  df-ring 20285  df-subrng 20596  df-subrg 20620  df-psr 21961  df-mpl 21963  df-opsr 21965  df-psr1 22242  df-ply1 22244

This theorem is referenced by:  ply1ascl0  22316  ply1ascl1  22317  coe1z  22326  coe1add  22327  coe1subfv  22329  ply1moncl  22334  coe1pwmul  22342  ply1sclf  22348  ply1scl0  22353  ply1scl1  22355  ply1coefsupp  22360  ply1coe  22361  cply1coe0bi  22365  coe1fzgsumdlem  22366  gsumsmonply1  22370  gsummoncoe1  22371  lply1binom  22373  lply1binomsc  22374  evls1sca  22386  evls1gsumadd  22387  evl1expd  22408  evl1gsumdlem  22419  evl1scvarpw  22426  evl1scvarpwval  22427  evl1gsummon  22428  evls1fpws  22432  evls1addd  22434  evls1muld  22435  rhmply1mon  22449  pmatring  22752  pmatlmod  22753  pmat0op  22755  pmat1op  22756  pmat1ovd  22757  1pmatscmul  22762  cpmatacl  22776  cpmatinvcl  22777  cpmatmcllem  22778  cpmatmcl  22779  mat2pmatbas  22786  mat2pmatghm  22790  mat2pmatmul  22791  mat2pmat1  22792  mat2pmatmhm  22793  mat2pmatrhm  22794  mat2pmatlin  22795  mat2pmatscmxcl  22800  m2pmfzgsumcl  22808  decpmatmullem  22831  pmatcollpw1  22836  pmatcollpw2lem  22837  pmatcollpw2  22838  monmatcollpw  22839  pmatcollpwlem  22840  pmatcollpw  22841  pmatcollpwfi  22842  pmatcollpw3fi1lem1  22846  pmatcollpwscmatlem1  22849  pmatcollpwscmatlem2  22850  pm2mpcl  22857  idpm2idmp  22861  mply1topmatcllem  22863  mply1topmatcl  22865  mp2pm2mplem2  22867  mp2pm2mplem4  22869  mp2pm2mp  22871  pm2mpghm  22876  pm2mpmhmlem2  22879  pm2mpmhm  22880  pm2mprhm  22881  monmat2matmon  22884  pm2mp  22885  chmatcl  22888  chmatval  22889  chpmat0d  22894  chpmat1dlem  22895  chpmat1d  22896  chpdmatlem0  22897  chpdmatlem2  22899  chpdmatlem3  22900  chpscmat  22902  chpscmatgsumbin  22904  chpscmatgsummon  22905  chp0mat  22906  chpidmat  22907  chmaidscmat  22908  chfacfscmulcl  22917  chfacfscmul0  22918  cpmadugsumlemB  22934  cpmadugsumlemC  22935  cpmadugsumlemF  22936  deg1addle2  26162  deg1add  26163  deg1suble  26167  deg1sub  26168  deg1sublt  26170  deg1mul2  26174  deg1mul3  26176  deg1mul3le  26177  deg1pw  26181  ply1nz  26182  ply1domn  26184  ply1divmo  26196  ply1divex  26197  uc1pmon1p  26212  r1pcl  26219  r1pid  26221  dvdsq1p  26223  dvdsr1p  26224  ply1remlem  26225  ply1rem  26226  idomrootle  26233  ig1peu  26235  ig1pval2  26237  ig1pdvds  26240  ig1prsp  26241  ply1lpir  26242  plypf1  26272  lgsqrlem2  27411  lgsqrlem3  27412  lgsqrlem4  27413  ressasclcl  33767  evls1subd  33768  ply1unit  33771  evls1monply1  33775  m1pmeq  33781  ply1coedeg  33785  ply1degltel  33790  ply1degleel  33791  ply1degltlss  33792  gsummoncoe1fzo  33793  ply1gsumz  33795  deg1addlt  33796  ig1pnunit  33797  q1pdir  33799  q1pvsca  33800  r1pvsca  33801  r1p0  33802  r1pcyc  33803  r1padd1  33804  r1pid2OLD  33805  r1plmhm  33806  r1pquslmic  33807  selvply1rhmlem4  33820  selvply1rhm  33822  vietadeg1  33875  ply1degltdimlem  33919  ply1degltdim  33920  extdgfialglem2  33990  ply1annnr  34000  irngnminplynz  34009  minplym1p  34010  minplynzm1p  34011  irredminply  34013  algextdeglem6  34019  algextdeglem8  34021  rtelextdg2lem  34023  2sqr3minply  34077  cos9thpiminplylem6  34084  cos9thpiminply  34085  ply1divalg3  35992  aks6d1c1p6  42731  aks6d1c6lem1  42787  aks6d1c6lem2  42788  hbtlem2  43701  hbtlem4  43703  hbtlem5  43705  hbtlem6  43706  hbt  43707  ply1sclrmsm  49006  ply1mulgsumlem4  49011  ply1mulgsum  49012  linply1  49015