ply1crng

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

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

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

Metamath Proof Explorer