Metamath Proof Explorer

Theorem ply1ring

Description: Univariate polynomials form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)

Ref Expression
Hypothesis ply1ring.p 
|- P = ( Poly1 ` R )
Assertion ply1ring 
|- ( R e. Ring -> P e. Ring )

Proof

Step Hyp Ref Expression
1 ply1ring.p 
 |-  P = ( Poly1 ` R )
2 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
3 eqid 
 |-  ( Base ` P ) = ( Base ` P )
4 1 2 3 ply1bas 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
5 1 2 3 ply1subrg 
 |-  ( R e. Ring -> ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) )
6 4 5 eqeltrrid 
 |-  ( R e. Ring -> ( Base ` ( 1o mPoly R ) ) e. ( SubRing ` ( PwSer1 ` R ) ) )
7 1 2 ply1val 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
8 7 subrgring 
 |-  ( ( Base ` ( 1o mPoly R ) ) e. ( SubRing ` ( PwSer1 ` R ) ) -> P e. Ring )
9 6 8 syl 
 |-  ( R e. Ring -> P e. Ring )