Theorem ply1ring 22224

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 2737	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22171	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2737	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22174	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2842	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22170	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20545	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 17	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7361  1_oc1o 8392  Basecbs 17173  Ringcrg 20208  SubRingcsubrg 20540   mPoly cmpl 21899  PwSer₁cps1 22151  Poly₁cpl1 22153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7625  df-ofr 7626  df-om 7812  df-1st 7936  df-2nd 7937  df-supp 8105  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-oi 9419  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245  df-n0 12432  df-z 12519  df-dec 12639  df-uz 12783  df-fz 13456  df-fzo 13603  df-seq 13958  df-hash 14287  df-struct 17111  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-mulr 17228  df-sca 17230  df-vsca 17231  df-ip 17232  df-tset 17233  df-ple 17234  df-ds 17236  df-hom 17238  df-cco 17239  df-0g 17398  df-gsum 17399  df-prds 17404  df-pws 17406  df-mre 17542  df-mrc 17543  df-acs 17545  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-mhm 18745  df-submnd 18746  df-grp 18906  df-minusg 18907  df-mulg 19038  df-subg 19093  df-ghm 19182  df-cntz 19286  df-cmn 19751  df-abl 19752  df-mgp 20116  df-rng 20128  df-ur 20157  df-ring 20210  df-subrng 20517  df-subrg 20541  df-psr 21902  df-mpl 21904  df-opsr 21906  df-psr1 22156  df-ply1 22158

This theorem is referenced by:  ply1ascl0  22231  ply1ascl1  22232  coe1z  22241  coe1add  22242  coe1subfv  22244  ply1moncl  22249  coe1pwmul  22257  ply1sclf  22263  ply1scl0  22268  ply1scl1  22270  ply1coefsupp  22275  ply1coe  22276  cply1coe0bi  22280  coe1fzgsumdlem  22281  gsumsmonply1  22285  gsummoncoe1  22286  lply1binom  22288  lply1binomsc  22289  evls1sca  22301  evls1gsumadd  22302  evl1expd  22323  evl1gsumdlem  22334  evl1scvarpw  22341  evl1scvarpwval  22342  evl1gsummon  22343  evls1fpws  22347  evls1addd  22349  evls1muld  22350  rhmply1mon  22367  pmatring  22670  pmatlmod  22671  pmat0op  22673  pmat1op  22674  pmat1ovd  22675  1pmatscmul  22680  cpmatacl  22694  cpmatinvcl  22695  cpmatmcllem  22696  cpmatmcl  22697  mat2pmatbas  22704  mat2pmatghm  22708  mat2pmatmul  22709  mat2pmat1  22710  mat2pmatmhm  22711  mat2pmatrhm  22712  mat2pmatlin  22713  mat2pmatscmxcl  22718  m2pmfzgsumcl  22726  decpmatmullem  22749  pmatcollpw1  22754  pmatcollpw2lem  22755  pmatcollpw2  22756  monmatcollpw  22757  pmatcollpwlem  22758  pmatcollpw  22759  pmatcollpwfi  22760  pmatcollpw3fi1lem1  22764  pmatcollpwscmatlem1  22767  pmatcollpwscmatlem2  22768  pm2mpcl  22775  idpm2idmp  22779  mply1topmatcllem  22781  mply1topmatcl  22783  mp2pm2mplem2  22785  mp2pm2mplem4  22787  mp2pm2mp  22789  pm2mpghm  22794  pm2mpmhmlem2  22797  pm2mpmhm  22798  pm2mprhm  22799  monmat2matmon  22802  pm2mp  22803  chmatcl  22806  chmatval  22807  chpmat0d  22812  chpmat1dlem  22813  chpmat1d  22814  chpdmatlem0  22815  chpdmatlem2  22817  chpdmatlem3  22818  chpscmat  22820  chpscmatgsumbin  22822  chpscmatgsummon  22823  chp0mat  22824  chpidmat  22825  chmaidscmat  22826  chfacfscmulcl  22835  chfacfscmul0  22836  cpmadugsumlemB  22852  cpmadugsumlemC  22853  cpmadugsumlemF  22854  deg1addle2  26080  deg1add  26081  deg1suble  26085  deg1sub  26086  deg1sublt  26088  deg1mul2  26092  deg1mul3  26094  deg1mul3le  26095  deg1pw  26099  ply1nz  26100  ply1domn  26102  ply1divmo  26114  ply1divex  26115  uc1pmon1p  26130  r1pcl  26137  r1pid  26139  dvdsq1p  26141  dvdsr1p  26142  ply1remlem  26143  ply1rem  26144  idomrootle  26151  ig1peu  26153  ig1pval2  26155  ig1pdvds  26158  ig1prsp  26159  ply1lpir  26160  plypf1  26190  lgsqrlem2  27327  lgsqrlem3  27328  lgsqrlem4  27329  ressasclcl  33649  evls1subd  33650  ply1unit  33653  evls1monply1  33657  m1pmeq  33663  ply1coedeg  33667  ply1degltel  33672  ply1degleel  33673  ply1degltlss  33674  gsummoncoe1fzo  33675  ply1gsumz  33677  deg1addlt  33678  ig1pnunit  33679  q1pdir  33681  q1pvsca  33682  r1pvsca  33683  r1p0  33684  r1pcyc  33685  r1padd1  33686  r1pid2OLD  33687  r1plmhm  33688  r1pquslmic  33689  vietadeg1  33740  ply1degltdimlem  33785  ply1degltdim  33786  extdgfialglem2  33856  ply1annnr  33866  irngnminplynz  33875  minplym1p  33876  minplynzm1p  33877  irredminply  33879  algextdeglem6  33885  algextdeglem8  33887  rtelextdg2lem  33889  2sqr3minply  33943  cos9thpiminplylem6  33950  cos9thpiminply  33951  ply1divalg3  35843  aks6d1c1p6  42570  aks6d1c6lem1  42626  aks6d1c6lem2  42627  hbtlem2  43573  hbtlem4  43575  hbtlem5  43577  hbtlem6  43578  hbt  43579  ply1sclrmsm  48875  ply1mulgsumlem4  48880  ply1mulgsum  48881  linply1  48884