This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
Assertion mpllmod ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )

Proof

Step Hyp Ref Expression
1 mplgrp.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
3 simpl ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝐼 ∈ 𝑉 )
4 simpr ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Ring )
5 2 3 4 psrlmod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( 𝐼 mPwSer 𝑅 ) ∈ LMod )
6 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
7 2 1 6 3 4 mpllss ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
8 1 2 6 mplval2 ⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s ( Base ‘ 𝑃 ) )
9 eqid ⊢ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) )
10 8 9 lsslmod ⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ LMod ∧ ( Base ‘ 𝑃 ) ∈ ( LSubSp ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑃 ∈ LMod )
11 5 7 10 syl2anc ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )