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 )