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 )