This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )