Theorem ply1ring 22475

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 2760	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22423	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2760	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22425	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2865	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22422	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20739	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 18	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7414  1_oc1o 8451  Basecbs 17304  Ringcrg 20375  SubRingcsubrg 20734   mPoly cmpl 22124  PwSer₁cps1 22403  Poly₁cpl1 22405

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-mulcom 11191  ax-addass 11192  ax-mulass 11193  ax-distr 11194  ax-i2m1 11195  ax-1ne0 11196  ax-1rid 11197  ax-rnegex 11198  ax-rrecex 11199  ax-cnre 11200  ax-pre-lttri 11201  ax-pre-lttrn 11202  ax-pre-ltadd 11203  ax-pre-mulgt0 11204

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7371  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-ofr 7680  df-om 7864  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8281  df-wrecs 8312  df-recs 8361  df-rdg 8400  df-1o 8458  df-2o 8459  df-er 8699  df-map 8831  df-pm 8832  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9335  df-sup 9415  df-oi 9485  df-card 9947  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11470  df-neg 11471  df-nn 12261  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12532  df-z 12619  df-dec 12740  df-uz 12891  df-fz 13565  df-fzo 13713  df-seq 14069  df-hash 14398  df-struct 17242  df-sets 17259  df-slot 17277  df-ndx 17289  df-base 17305  df-ress 17326  df-plusg 17358  df-mulr 17359  df-sca 17361  df-vsca 17362  df-ip 17363  df-tset 17364  df-ple 17365  df-ds 17367  df-hom 17369  df-cco 17370  df-0g 17529  df-gsum 17530  df-prds 17535  df-pws 17537  df-mre 17673  df-mrc 17674  df-acs 17676  df-mgm 18733  df-sgrp 18824  df-mnd 18840  df-mhm 18894  df-submnd 18895  df-grp 19063  df-minusg 19064  df-mulg 19194  df-subg 19249  df-ghm 19344  df-cntz 19447  df-cmn 19912  df-abl 19913  df-mgp 20277  df-rng 20291  df-ur 20324  df-ring 20377  df-subrng 20711  df-subrg 20735  df-psr 22127  df-mpl 22129  df-opsr 22131  df-psr1 22408  df-ply1 22410

This theorem is used by:  ply1ascl0  22482  ply1ascl1  22483  coe1z  22492  coe1add  22493  coe1subfv  22495  ply1moncl  22500  coe1pwmul  22508  ply1sclf  22514  ply1scl0  22519  ply1scl1  22521  ply1coefsupp  22525  ply1coe  22526  cply1coe0bi  22530  coe1fzgsumdlem  22531  gsumsmonply1  22535  gsummoncoe1  22536  lply1binom  22538  lply1binomsc  22539  evls1sca  22551  evls1gsumadd  22552  evl1expd  22573  evl1gsumdlem  22584  evl1scvarpw  22591  evl1scvarpwval  22592  evl1gsummon  22593  evls1fpws  22597  evls1addd  22599  evls1muld  22600  rhmply1mon  22614  pmatring  22920  pmatlmod  22921  pmat0op  22923  pmat1op  22924  pmat1ovd  22925  1pmatscmul  22930  cpmatacl  22944  cpmatinvcl  22945  cpmatmcllem  22946  cpmatmcl  22947  mat2pmatbas  22954  mat2pmatghm  22958  mat2pmatmul  22959  mat2pmat1  22960  mat2pmatmhm  22961  mat2pmatrhm  22962  mat2pmatlin  22963  mat2pmatscmxcl  22968  m2pmfzgsumcl  22976  decpmatmullem  22999  pmatcollpw1  23004  pmatcollpw2lem  23005  pmatcollpw2  23006  monmatcollpw  23007  pmatcollpwlem  23008  pmatcollpw  23009  pmatcollpwfi  23010  pmatcollpw3fi1lem1  23014  pmatcollpwscmatlem1  23017  pmatcollpwscmatlem2  23018  pm2mpcl  23025  idpm2idmp  23029  mply1topmatcllem  23031  mply1topmatcl  23033  mp2pm2mplem2  23035  mp2pm2mplem4  23037  mp2pm2mp  23039  pm2mpghm  23044  pm2mpmhmlem2  23047  pm2mpmhm  23048  pm2mprhm  23049  monmat2matmon  23052  pm2mp  23053  chmatcl  23056  chmatval  23057  chpmat0d  23062  chpmat1dlem  23063  chpmat1d  23064  chpdmatlem0  23065  chpdmatlem2  23067  chpdmatlem3  23068  chpscmat  23070  chpscmatgsumbin  23072  chpscmatgsummon  23073  chp0mat  23074  chpidmat  23075  chmaidscmat  23076  chfacfscmulcl  23085  chfacfscmul0  23086  cpmadugsumlemB  23102  cpmadugsumlemC  23103  cpmadugsumlemF  23104  deg1addle2  26330  deg1add  26331  deg1suble  26335  deg1sub  26336  deg1sublt  26338  deg1mul2  26342  deg1mul3  26344  deg1mul3le  26345  deg1pw  26349  ply1nz  26350  ply1domn  26352  ply1divmo  26364  ply1divex  26365  uc1pmon1p  26380  r1pcl  26387  r1pid  26389  dvdsq1p  26391  dvdsr1p  26392  ply1remlem  26393  ply1rem  26394  idomrootle  26401  ig1peu  26403  ig1pval2  26405  ig1pdvds  26408  ig1prsp  26409  ply1lpir  26410  plypf1  26441  lgsqrlem2  27586  lgsqrlem3  27587  lgsqrlem4  27588  ressasclcl  33984  evls1subd  33985  ply1unit  33988  evls1monply1  33992  m1pmeq  33998  ply1coedeg  34002  ply1degltel  34007  ply1degleel  34008  ply1degltlss  34009  gsummoncoe1fzo  34010  ply1gsumz  34012  deg1addlt  34013  ig1pnunit  34014  q1pdir  34016  q1pvsca  34017  r1pvsca  34018  r1p0  34019  r1pcyc  34020  r1padd1  34021  r1plmhm  34022  r1pquslmic  34023  selvply1rhmlem4  34036  selvply1rhm  34038  vietadeg1  34091  ply1degltdimlem  34135  ply1degltdim  34136  extdgfialglem2  34206  ply1annnr  34216  irngnminplynz  34225  minplym1p  34226  minplynzm1p  34227  irredminply  34229  algextdeglem6  34235  algextdeglem8  34237  rtelextdg2lem  34239  2sqr3minply  34293  cos9thpiminplylem6  34300  cos9thpiminply  34301  ply1divalg3  36224  aks6d1c1p6  42983  aks6d1c6lem1  43039  aks6d1c6lem2  43040  hbtlem2  43968  hbtlem4  43970  hbtlem5  43972  hbtlem6  43973  hbt  43974  ply1sclrmsm  49317  ply1mulgsumlem4  49322  ply1mulgsum  49323  linply1  49326