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	|- ( ph -> I e. V )
	mpllmodd.r	|- ( ph -> R e. Ring )
Assertion	mpllmodd	|- ( ph -> P e. LMod )

Proof

Step	Hyp	Ref	Expression
1		mpllmodd.p	|- P = ( I mPoly R )
2		mpllmodd.i	|- ( ph -> I e. V )
3		mpllmodd.r	|- ( ph -> R e. Ring )
4	1	mpllmod	|- ( ( I e. V /\ R e. Ring ) -> P e. LMod )
5	2 3 4	syl2anc	|- ( ph -> P e. LMod )