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

Metamath Proof Explorer

Theorem mpllmodd

Description: The polynomial ring is a left module. (Contributed by SN, 12-Mar-2025)

Ref Expression
Hypotheses mpllmodd.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mpllmodd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mpllmodd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion mpllmodd ( 𝜑 → 𝑃 ∈ LMod )

Proof

Step Hyp Ref Expression
1 mpllmodd.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mpllmodd.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 mpllmodd.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 1 mpllmod ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ LMod )
5 2 3 4 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ LMod )