Theorem ply1ring 22577

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 2763	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3	1, 2	ply1bas 22525	. . 3 ⊢ (Base‘𝑃) = (Base‘(1o mPoly 𝑅))
4		eqid 2763	. . . 4 ⊢ (PwSer1‘𝑅) = (PwSer1‘𝑅)
5	1, 4, 2	ply1subrg 22527	. . 3 ⊢ (𝑅 ∈ Ring → (Base‘𝑃) ∈ (SubRing‘(PwSer1‘𝑅)))
6	3, 5	eqeltrrid 2868	. 2 ⊢ (𝑅 ∈ Ring → (Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)))
7	1, 4	ply1val 22524	. . 3 ⊢ 𝑃 = ((PwSer1‘𝑅) ↾s (Base‘(1o mPoly 𝑅)))
8	7	subrgring 20838	. 2 ⊢ ((Base‘(1o mPoly 𝑅)) ∈ (SubRing‘(PwSer1‘𝑅)) → 𝑃 ∈ Ring)
9	6, 8	syl 18	1 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  ‘cfv 6546  (class class class)co 7427  1_oc1o 8480  Basecbs 17399  Ringcrg 20471  SubRingcsubrg 20833   mPoly cmpl 22226  PwSer₁cps1 22505  Poly₁cpl1 22507

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5234  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-cnex 11266  ax-resscn 11267  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-mulcom 11274  ax-addass 11275  ax-mulass 11276  ax-distr 11277  ax-i2m1 11278  ax-1ne0 11279  ax-1rid 11280  ax-rnegex 11281  ax-rrecex 11282  ax-cnre 11283  ax-pre-lttri 11284  ax-pre-lttrn 11285  ax-pre-ltadd 11286  ax-pre-mulgt0 11287

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3368  df-reu 3369  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-pss 4016  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4838  df-uni 4870  df-int 4910  df-iun 4955  df-iin 4956  df-br 5106  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5549  df-eprel 5554  df-po 5562  df-so 5563  df-fr 5607  df-se 5608  df-we 5609  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6310  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-isom 6555  df-riota 7384  df-ov 7430  df-oprab 7431  df-mpo 7432  df-of 7700  df-ofr 7701  df-om 7885  df-1st 8008  df-2nd 8009  df-supp 8188  df-frecs 8310  df-wrecs 8341  df-recs 8390  df-rdg 8429  df-1o 8487  df-2o 8488  df-er 8728  df-map 8860  df-pm 8861  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9365  df-sup 9444  df-oi 9514  df-card 10030  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359  df-sub 11553  df-neg 11554  df-nn 12346  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420  df-8 12421  df-9 12422  df-n0 12617  df-z 12704  df-dec 12825  df-uz 12976  df-fz 13650  df-fzo 13799  df-seq 14155  df-hash 14485  df-struct 17337  df-sets 17354  df-slot 17372  df-ndx 17384  df-base 17400  df-ress 17421  df-plusg 17453  df-mulr 17454  df-sca 17456  df-vsca 17457  df-ip 17458  df-tset 17459  df-ple 17460  df-ds 17462  df-hom 17464  df-cco 17465  df-0g 17624  df-gsum 17625  df-prds 17630  df-pws 17632  df-mre 17768  df-mrc 17769  df-acs 17771  df-mgm 18828  df-sgrp 18920  df-mnd 18936  df-mhm 18990  df-submnd 18991  df-grp 19159  df-minusg 19160  df-mulg 19290  df-subg 19345  df-ghm 19440  df-cntz 19543  df-cmn 20008  df-abl 20009  df-mgp 20373  df-rng 20387  df-ur 20420  df-ring 20473  df-subrng 20810  df-subrg 20834  df-psr 22229  df-mpl 22231  df-opsr 22233  df-psr1 22510  df-ply1 22512

This theorem is used by:  ply1ascl0  22584  ply1ascl1  22585  coe1z  22594  coe1add  22595  coe1subfv  22597  ply1moncl  22602  coe1pwmul  22610  ply1sclf  22616  ply1scl0  22621  ply1scl1  22623  ply1coefsupp  22627  ply1coe  22628  cply1coe0bi  22632  coe1fzgsumdlem  22633  gsumsmonply1  22637  gsummoncoe1  22638  lply1binom  22640  lply1binomsc  22641  evls1sca  22653  evls1gsumadd  22654  evl1expd  22675  evl1gsumdlem  22686  evl1scvarpw  22693  evl1scvarpwval  22694  evl1gsummon  22695  evls1fpws  22699  evls1addd  22701  evls1muld  22702  rhmply1mon  22716  pmatring  23022  pmatlmod  23023  pmat0op  23025  pmat1op  23026  pmat1ovd  23027  1pmatscmul  23032  cpmatacl  23046  cpmatinvcl  23047  cpmatmcllem  23048  cpmatmcl  23049  mat2pmatbas  23056  mat2pmatghm  23060  mat2pmatmul  23061  mat2pmat1  23062  mat2pmatmhm  23063  mat2pmatrhm  23064  mat2pmatlin  23065  mat2pmatscmxcl  23070  m2pmfzgsumcl  23078  decpmatmullem  23101  pmatcollpw1  23106  pmatcollpw2lem  23107  pmatcollpw2  23108  monmatcollpw  23109  pmatcollpwlem  23110  pmatcollpw  23111  pmatcollpwfi  23112  pmatcollpw3fi1lem1  23116  pmatcollpwscmatlem1  23119  pmatcollpwscmatlem2  23120  pm2mpcl  23127  idpm2idmp  23131  mply1topmatcllem  23133  mply1topmatcl  23135  mp2pm2mplem2  23137  mp2pm2mplem4  23139  mp2pm2mp  23141  pm2mpghm  23146  pm2mpmhmlem2  23149  pm2mpmhm  23150  pm2mprhm  23151  monmat2matmon  23154  pm2mp  23155  chmatcl  23158  chmatval  23159  chpmat0d  23164  chpmat1dlem  23165  chpmat1d  23166  chpdmatlem0  23167  chpdmatlem2  23169  chpdmatlem3  23170  chpscmat  23172  chpscmatgsumbin  23174  chpscmatgsummon  23175  chp0mat  23176  chpidmat  23177  chmaidscmat  23178  chfacfscmulcl  23187  chfacfscmul0  23188  cpmadugsumlemB  23204  cpmadugsumlemC  23205  cpmadugsumlemF  23206  deg1addle2  26432  deg1add  26433  deg1suble  26437  deg1sub  26438  deg1sublt  26440  deg1mul2  26444  deg1mul3  26446  deg1mul3le  26447  deg1pw  26451  ply1nz  26452  ply1domn  26454  ply1divmo  26466  ply1divex  26467  uc1pmon1p  26482  r1pcl  26489  r1pid  26491  dvdsq1p  26493  dvdsr1p  26494  ply1remlem  26495  ply1rem  26496  idomrootle  26503  ig1peu  26505  ig1pval2  26507  ig1pdvds  26510  ig1prsp  26511  ply1lpir  26512  plypf1  26543  lgsqrlem2  27686  lgsqrlem3  27687  lgsqrlem4  27688  ressasclcl  34156  evls1subd  34157  ply1unit  34160  evls1monply1  34164  m1pmeq  34170  ply1coedeg  34174  ply1degltel  34179  ply1degleel  34180  ply1degltlss  34181  gsummoncoe1fzo  34182  ply1gsumz  34184  deg1addlt  34185  ig1pnunit  34186  q1pdir  34188  q1pvsca  34189  r1pvsca  34190  r1p0  34191  r1pcyc  34192  r1padd1  34193  r1plmhm  34194  r1pquslmic  34195  selvply1rhmlem4  34208  selvply1rhm  34210  vietadeg1  34263  ply1degltdimlem  34307  ply1degltdim  34308  extdgfialglem2  34378  ply1annnr  34388  irngnminplynz  34397  minplym1p  34398  minplynzm1p  34399  irredminply  34401  algextdeglem6  34407  algextdeglem8  34409  rtelextdg2lem  34411  2sqr3minply  34465  cos9thpiminplylem6  34472  cos9thpiminply  34473  ply1divalg3  36528  aks6d1c1p6  43304  aks6d1c6lem1  43360  aks6d1c6lem2  43361  hbtlem2  44266  hbtlem4  44268  hbtlem5  44270  hbtlem6  44271  hbt  44272  ply1sclrmsm  49635  ply1mulgsumlem4  49640  ply1mulgsum  49641  linply1  49644