ply1ring

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

		Ref	Expression
	Hypothesis	ply1ring.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1ring	$⊢ R \in Ring \to P \in Ring$

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

Metamath Proof Explorer