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 ⊢ P = I mPoly R
mpllmodd.i ⊢ φ → I ∈ V
mpllmodd.r ⊢ φ → R ∈ Ring
Assertion mpllmodd ⊢ φ → P ∈ LMod

Proof

Step Hyp Ref Expression
1 mpllmodd.p ⊢ P = I mPoly R
2 mpllmodd.i ⊢ φ → I ∈ V
3 mpllmodd.r ⊢ φ → R ∈ Ring
4 1 mpllmod ⊢ I ∈ V ∧ R ∈ Ring → P ∈ LMod
5 2 3 4 syl2anc ⊢ φ → P ∈ LMod