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