Theorem ply1ring 22132

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 2729	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22079	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2729	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22082	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2833	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22078	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20483	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  1_oc1o 8427  Basecbs 17179  Ringcrg 20142  SubRingcsubrg 20478   mPoly cmpl 21815  PwSer₁cps1 22059  Poly₁cpl1 22061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-iin 4958  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-of 7653  df-ofr 7654  df-om 7843  df-1st 7968  df-2nd 7969  df-supp 8140  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-2o 8435  df-er 8671  df-map 8801  df-pm 8802  df-ixp 8871  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-fsupp 9313  df-sup 9393  df-oi 9463  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-z 12530  df-dec 12650  df-uz 12794  df-fz 13469  df-fzo 13616  df-seq 13967  df-hash 14296  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 17547  df-mrc 17548  df-acs 17550  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 19145  df-cntz 19249  df-cmn 19712  df-abl 19713  df-mgp 20050  df-rng 20062  df-ur 20091  df-ring 20144  df-subrng 20455  df-subrg 20479  df-psr 21818  df-mpl 21820  df-opsr 21822  df-psr1 22064  df-ply1 22066

This theorem is referenced by:  ply1ascl0  22139  ply1ascl1  22140  coe1z  22149  coe1add  22150  coe1subfv  22152  ply1moncl  22157  coe1pwmul  22165  ply1sclf  22171  ply1scl0  22176  ply1scl0OLD  22177  ply1scl1  22179  ply1scl1OLD  22180  ply1coefsupp  22184  ply1coe  22185  cply1coe0bi  22189  coe1fzgsumdlem  22190  gsumsmonply1  22194  gsummoncoe1  22195  lply1binom  22197  lply1binomsc  22198  evls1sca  22210  evls1gsumadd  22211  evl1expd  22232  evl1gsumdlem  22243  evl1scvarpw  22250  evl1scvarpwval  22251  evl1gsummon  22252  evls1fpws  22256  evls1addd  22258  evls1muld  22259  rhmply1mon  22276  pmatring  22579  pmatlmod  22580  pmat0op  22582  pmat1op  22583  pmat1ovd  22584  1pmatscmul  22589  cpmatacl  22603  cpmatinvcl  22604  cpmatmcllem  22605  cpmatmcl  22606  mat2pmatbas  22613  mat2pmatghm  22617  mat2pmatmul  22618  mat2pmat1  22619  mat2pmatmhm  22620  mat2pmatrhm  22621  mat2pmatlin  22622  mat2pmatscmxcl  22627  m2pmfzgsumcl  22635  decpmatmullem  22658  pmatcollpw1  22663  pmatcollpw2lem  22664  pmatcollpw2  22665  monmatcollpw  22666  pmatcollpwlem  22667  pmatcollpw  22668  pmatcollpwfi  22669  pmatcollpw3fi1lem1  22673  pmatcollpwscmatlem1  22676  pmatcollpwscmatlem2  22677  pm2mpcl  22684  idpm2idmp  22688  mply1topmatcllem  22690  mply1topmatcl  22692  mp2pm2mplem2  22694  mp2pm2mplem4  22696  mp2pm2mp  22698  pm2mpghm  22703  pm2mpmhmlem2  22706  pm2mpmhm  22707  pm2mprhm  22708  monmat2matmon  22711  pm2mp  22712  chmatcl  22715  chmatval  22716  chpmat0d  22721  chpmat1dlem  22722  chpmat1d  22723  chpdmatlem0  22724  chpdmatlem2  22726  chpdmatlem3  22727  chpscmat  22729  chpscmatgsumbin  22731  chpscmatgsummon  22732  chp0mat  22733  chpidmat  22734  chmaidscmat  22735  chfacfscmulcl  22744  chfacfscmul0  22745  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  deg1addle2  26007  deg1add  26008  deg1suble  26012  deg1sub  26013  deg1sublt  26015  deg1mul2  26019  deg1mul3  26021  deg1mul3le  26022  deg1pw  26026  ply1nz  26027  ply1domn  26029  ply1divmo  26041  ply1divex  26042  uc1pmon1p  26057  r1pcl  26064  r1pid  26066  dvdsq1p  26068  dvdsr1p  26069  ply1remlem  26070  ply1rem  26071  idomrootle  26078  ig1peu  26080  ig1pval2  26082  ig1pdvds  26085  ig1prsp  26086  ply1lpir  26087  plypf1  26117  lgsqrlem2  27258  lgsqrlem3  27259  lgsqrlem4  27260  ressasclcl  33540  evls1subd  33541  ply1unit  33544  m1pmeq  33552  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  gsummoncoe1fzo  33563  ply1gsumz  33564  deg1addlt  33565  ig1pnunit  33566  q1pdir  33568  q1pvsca  33569  r1pvsca  33570  r1p0  33571  r1pcyc  33572  r1padd1  33573  r1pid2OLD  33574  r1plmhm  33575  r1pquslmic  33576  ply1degltdimlem  33618  ply1degltdim  33619  ply1annnr  33693  irngnminplynz  33702  minplym1p  33703  minplynzm1p  33704  irredminply  33706  algextdeglem6  33712  algextdeglem8  33714  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminplylem6  33777  cos9thpiminply  33778  ply1divalg3  35629  aks6d1c1p6  42102  aks6d1c6lem1  42158  aks6d1c6lem2  42159  hbtlem2  43113  hbtlem4  43115  hbtlem5  43117  hbtlem6  43118  hbt  43119  ply1sclrmsm  48372  ply1mulgsumlem4  48378  ply1mulgsum  48379  linply1  48382