Theorem ply1ring 22186

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 22133	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2734	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22136	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2839	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22132	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20505	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  1_oc1o 8388  Basecbs 17134  Ringcrg 20166  SubRingcsubrg 20500   mPoly cmpl 21860  PwSer₁cps1 22113  Poly₁cpl1 22115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-iin 4947  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-se 5576  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-isom 6499  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-ofr 7621  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8763  df-pm 8764  df-ixp 8834  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-fsupp 9263  df-sup 9343  df-oi 9413  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-2 12206  df-3 12207  df-4 12208  df-5 12209  df-6 12210  df-7 12211  df-8 12212  df-9 12213  df-n0 12400  df-z 12487  df-dec 12606  df-uz 12750  df-fz 13422  df-fzo 13569  df-seq 13923  df-hash 14252  df-struct 17072  df-sets 17089  df-slot 17107  df-ndx 17119  df-base 17135  df-ress 17156  df-plusg 17188  df-mulr 17189  df-sca 17191  df-vsca 17192  df-ip 17193  df-tset 17194  df-ple 17195  df-ds 17197  df-hom 17199  df-cco 17200  df-0g 17359  df-gsum 17360  df-prds 17365  df-pws 17367  df-mre 17503  df-mrc 17504  df-acs 17506  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-mhm 18706  df-submnd 18707  df-grp 18864  df-minusg 18865  df-mulg 18996  df-subg 19051  df-ghm 19140  df-cntz 19244  df-cmn 19709  df-abl 19710  df-mgp 20074  df-rng 20086  df-ur 20115  df-ring 20168  df-subrng 20477  df-subrg 20501  df-psr 21863  df-mpl 21865  df-opsr 21867  df-psr1 22118  df-ply1 22120

This theorem is referenced by:  ply1ascl0  22193  ply1ascl1  22194  coe1z  22203  coe1add  22204  coe1subfv  22206  ply1moncl  22211  coe1pwmul  22219  ply1sclf  22225  ply1scl0  22230  ply1scl0OLD  22231  ply1scl1  22233  ply1scl1OLD  22234  ply1coefsupp  22239  ply1coe  22240  cply1coe0bi  22244  coe1fzgsumdlem  22245  gsumsmonply1  22249  gsummoncoe1  22250  lply1binom  22252  lply1binomsc  22253  evls1sca  22265  evls1gsumadd  22266  evl1expd  22287  evl1gsumdlem  22298  evl1scvarpw  22305  evl1scvarpwval  22306  evl1gsummon  22307  evls1fpws  22311  evls1addd  22313  evls1muld  22314  rhmply1mon  22331  pmatring  22634  pmatlmod  22635  pmat0op  22637  pmat1op  22638  pmat1ovd  22639  1pmatscmul  22644  cpmatacl  22658  cpmatinvcl  22659  cpmatmcllem  22660  cpmatmcl  22661  mat2pmatbas  22668  mat2pmatghm  22672  mat2pmatmul  22673  mat2pmat1  22674  mat2pmatmhm  22675  mat2pmatrhm  22676  mat2pmatlin  22677  mat2pmatscmxcl  22682  m2pmfzgsumcl  22690  decpmatmullem  22713  pmatcollpw1  22718  pmatcollpw2lem  22719  pmatcollpw2  22720  monmatcollpw  22721  pmatcollpwlem  22722  pmatcollpw  22723  pmatcollpwfi  22724  pmatcollpw3fi1lem1  22728  pmatcollpwscmatlem1  22731  pmatcollpwscmatlem2  22732  pm2mpcl  22739  idpm2idmp  22743  mply1topmatcllem  22745  mply1topmatcl  22747  mp2pm2mplem2  22749  mp2pm2mplem4  22751  mp2pm2mp  22753  pm2mpghm  22758  pm2mpmhmlem2  22761  pm2mpmhm  22762  pm2mprhm  22763  monmat2matmon  22766  pm2mp  22767  chmatcl  22770  chmatval  22771  chpmat0d  22776  chpmat1dlem  22777  chpmat1d  22778  chpdmatlem0  22779  chpdmatlem2  22781  chpdmatlem3  22782  chpscmat  22784  chpscmatgsumbin  22786  chpscmatgsummon  22787  chp0mat  22788  chpidmat  22789  chmaidscmat  22790  chfacfscmulcl  22799  chfacfscmul0  22800  cpmadugsumlemB  22816  cpmadugsumlemC  22817  cpmadugsumlemF  22818  deg1addle2  26061  deg1add  26062  deg1suble  26066  deg1sub  26067  deg1sublt  26069  deg1mul2  26073  deg1mul3  26075  deg1mul3le  26076  deg1pw  26080  ply1nz  26081  ply1domn  26083  ply1divmo  26095  ply1divex  26096  uc1pmon1p  26111  r1pcl  26118  r1pid  26120  dvdsq1p  26122  dvdsr1p  26123  ply1remlem  26124  ply1rem  26125  idomrootle  26132  ig1peu  26134  ig1pval2  26136  ig1pdvds  26139  ig1prsp  26140  ply1lpir  26141  plypf1  26171  lgsqrlem2  27312  lgsqrlem3  27313  lgsqrlem4  27314  ressasclcl  33601  evls1subd  33602  ply1unit  33605  evls1monply1  33609  m1pmeq  33615  ply1coedeg  33619  ply1degltel  33624  ply1degleel  33625  ply1degltlss  33626  gsummoncoe1fzo  33627  ply1gsumz  33629  deg1addlt  33630  ig1pnunit  33631  q1pdir  33633  q1pvsca  33634  r1pvsca  33635  r1p0  33636  r1pcyc  33637  r1padd1  33638  r1pid2OLD  33639  r1plmhm  33640  r1pquslmic  33641  vietadeg1  33683  ply1degltdimlem  33728  ply1degltdim  33729  extdgfialglem2  33799  ply1annnr  33809  irngnminplynz  33818  minplym1p  33819  minplynzm1p  33820  irredminply  33822  algextdeglem6  33828  algextdeglem8  33830  rtelextdg2lem  33832  2sqr3minply  33886  cos9thpiminplylem6  33893  cos9thpiminply  33894  ply1divalg3  35785  aks6d1c1p6  42307  aks6d1c6lem1  42363  aks6d1c6lem2  42364  hbtlem2  43308  hbtlem4  43310  hbtlem5  43312  hbtlem6  43313  hbt  43314  ply1sclrmsm  48572  ply1mulgsumlem4  48577  ply1mulgsum  48578  linply1  48581