Theorem ply1ring

Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypothesis	ply1ring.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		ply1ring.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
3	1 2	ply1bas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
4		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
5	1 4 2	ply1subrg	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
6	3 5	eqeltrrid	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
7	1 4	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	7	subrgring	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\to P\in \mathrm{Ring}$$
9	6 8	syl	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$