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