Theorem mpllmodd

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

	Ref	Expression
Hypotheses	mpllmodd.p	$$⊢P=I\mathrm{mPoly}R$$
	mpllmodd.i	$$⊢\phi \to I\in V$$
	mpllmodd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mpllmodd	$$⊢\phi \to P\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		mpllmodd.p	$$⊢P=I\mathrm{mPoly}R$$
2		mpllmodd.i	$$⊢\phi \to I\in V$$
3		mpllmodd.r	$$⊢\phi \to R\in \mathrm{Ring}$$
4	1	mpllmod	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to P\in \mathrm{LMod}$$
5	2 3 4	syl2anc	$$⊢\phi \to P\in \mathrm{LMod}$$