Metamath Proof Explorer

Theorem ply1lmod

Description: Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 ply1lmod.p 
 |-  P = ( Poly1 ` R )
2 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
3 2 psr1lmod 
 |-  ( R e. Ring -> ( PwSer1 ` R ) e. LMod )
4 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
5 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
6 4 5 ply1bas 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( 1o mPoly R ) )
7 4 2 5 ply1lss 
 |-  ( R e. Ring -> ( Base ` ( Poly1 ` R ) ) e. ( LSubSp ` ( PwSer1 ` R ) ) )
8 6 7 eqeltrrid 
 |-  ( R e. Ring -> ( Base ` ( 1o mPoly R ) ) e. ( LSubSp ` ( PwSer1 ` R ) ) )
9 1 2 ply1val 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
10 eqid 
 |-  ( LSubSp ` ( PwSer1 ` R ) ) = ( LSubSp ` ( PwSer1 ` R ) )
11 9 10 lsslmod 
 |-  ( ( ( PwSer1 ` R ) e. LMod /\ ( Base ` ( 1o mPoly R ) ) e. ( LSubSp ` ( PwSer1 ` R ) ) ) -> P e. LMod )
12 3 8 11 syl2anc 
 |-  ( R e. Ring -> P e. LMod )