Theorem ply1crng

Description: The ring of univariate polynomials is a commutative ring. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypothesis	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1crng	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{CRing}$$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
3	2	psr1crng	$$⊢R\in \mathrm{CRing}\to {\mathrm{PwSer}}_1\left(R\right)\in \mathrm{CRing}$$
4		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
5	1 2 4	ply1bas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
6		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
7	1 2 4	ply1subrg	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
8	6 7	syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
9	5 8	eqeltrrid	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
10	1 2	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
11	10	subrgcrng	$$⊢\left({\mathrm{PwSer}}_1\left(R\right)\in \mathrm{CRing}\wedge {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\right)\to P\in \mathrm{CRing}$$
12	3 9 11	syl2anc	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{CRing}$$