Metamath Proof Explorer

Theorem mpllmod

Description: The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypothesis mplgrp.p 
|- P = ( I mPoly R )
Assertion mpllmod 
|- ( ( I e. V /\ R e. Ring ) -> P e. LMod )

Proof

Step Hyp Ref Expression
1 mplgrp.p 
 |-  P = ( I mPoly R )
2 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
3 simpl 
 |-  ( ( I e. V /\ R e. Ring ) -> I e. V )
4 simpr 
 |-  ( ( I e. V /\ R e. Ring ) -> R e. Ring )
5 2 3 4 psrlmod 
 |-  ( ( I e. V /\ R e. Ring ) -> ( I mPwSer R ) e. LMod )
6 eqid 
 |-  ( Base ` P ) = ( Base ` P )
7 2 1 6 3 4 mpllss 
 |-  ( ( I e. V /\ R e. Ring ) -> ( Base ` P ) e. ( LSubSp ` ( I mPwSer R ) ) )
8 1 2 6 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
9 eqid 
 |-  ( LSubSp ` ( I mPwSer R ) ) = ( LSubSp ` ( I mPwSer R ) )
10 8 9 lsslmod 
 |-  ( ( ( I mPwSer R ) e. LMod /\ ( Base ` P ) e. ( LSubSp ` ( I mPwSer R ) ) ) -> P e. LMod )
11 5 7 10 syl2anc 
 |-  ( ( I e. V /\ R e. Ring ) -> P e. LMod )