Theorem ply1crng

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

	Ref	Expression
Hypothesis	ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
Assertion	ply1crng	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
3	2	psr1crng	⊢ ( 𝑅 ∈ CRing → ( PwSer1 ‘ 𝑅 ) ∈ CRing )
4		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
5	1 4	ply1bas	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( 1o mPoly 𝑅 ) )
6		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7	1 2 4	ply1subrg	⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) )
8	6 7	syl	⊢ ( 𝑅 ∈ CRing → ( Base ‘ 𝑃 ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) )
9	5 8	eqeltrrid	⊢ ( 𝑅 ∈ CRing → ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) )
10	1 2	ply1val	⊢ 𝑃 = ( ( PwSer1 ‘ 𝑅 ) ↾s ( Base ‘ ( 1o mPoly 𝑅 ) ) )
11	10	subrgcrng	⊢ ( ( ( PwSer1 ‘ 𝑅 ) ∈ CRing ∧ ( Base ‘ ( 1o mPoly 𝑅 ) ) ∈ ( SubRing ‘ ( PwSer1 ‘ 𝑅 ) ) ) → 𝑃 ∈ CRing )
12	3 9 11	syl2anc	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ CRing )