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
|- P = ( Poly1 ` R )
Assertion ply1crng
|- ( R e. CRing -> P e. CRing )

Proof

Step Hyp Ref Expression
1 ply1val.1
 |-  P = ( Poly1 ` R )
2 eqid
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
3 2 psr1crng
 |-  ( R e. CRing -> ( PwSer1 ` R ) e. CRing )
4 eqid
 |-  ( Base ` P ) = ( Base ` P )
5 1 2 4 ply1bas
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
6 crngring
 |-  ( R e. CRing -> R e. Ring )
7 1 2 4 ply1subrg
 |-  ( R e. Ring -> ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) )
8 6 7 syl
 |-  ( R e. CRing -> ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) )
9 5 8 eqeltrrid
 |-  ( R e. CRing -> ( Base ` ( 1o mPoly R ) ) e. ( SubRing ` ( PwSer1 ` R ) ) )
10 1 2 ply1val
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
11 10 subrgcrng
 |-  ( ( ( PwSer1 ` R ) e. CRing /\ ( Base ` ( 1o mPoly R ) ) e. ( SubRing ` ( PwSer1 ` R ) ) ) -> P e. CRing )
12 3 9 11 syl2anc
 |-  ( R e. CRing -> P e. CRing )