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 V R Ring P LMod

Proof

Step Hyp Ref Expression
1 mplgrp.p P = I mPoly R
2 eqid I mPwSer R = I mPwSer R
3 simpl I V R Ring I V
4 simpr I V R Ring R Ring
5 2 3 4 psrlmod I V R Ring I mPwSer R LMod
6 eqid Base P = Base P
7 2 1 6 3 4 mpllss I V R Ring Base P LSubSp I mPwSer R
8 1 2 6 mplval2 P = I mPwSer R 𝑠 Base P
9 eqid LSubSp I mPwSer R = LSubSp I mPwSer R
10 8 9 lsslmod I mPwSer R LMod Base P LSubSp I mPwSer R P LMod
11 5 7 10 syl2anc I V R Ring P LMod