mpllmod

Description: The polynomial ring is a left module. (Contributed by Mario Carneiro, 9-Jan-2015)

		Ref	Expression
	Hypothesis	mplgrp.p	$⊢ P = I mPoly R$
	Assertion	mpllmod	$⊢ (I \in V \land R \in Ring) \to P \in LMod$

Step	Hyp	Ref	Expression
1		mplgrp.p	$⊢ P = I mPoly R$
2		eqid	$⊢ I mPwSer R = I mPwSer R$
3		simpl	$⊢ (I \in V \land R \in Ring) \to I \in V$
4		simpr	$⊢ (I \in V \land R \in Ring) \to R \in Ring$
5	2 3 4	psrlmod	$⊢ (I \in V \land R \in Ring) \to I mPwSer R \in LMod$
6		eqid	$⊢ {Base}_{P} = {Base}_{P}$
7	2 1 6 3 4	mpllss	$⊢ (I \in V \land R \in Ring) \to {Base}_{P} \in LSubSp (I mPwSer R)$
8	1 2 6	mplval2	$⊢ P = (I mPwSer R) ↾_{𝑠} {Base}_{P}$
9		eqid	$⊢ LSubSp (I mPwSer R) = LSubSp (I mPwSer R)$
10	8 9	lsslmod	$⊢ (I mPwSer R \in LMod \land {Base}_{P} \in LSubSp (I mPwSer R)) \to P \in LMod$
11	5 7 10	syl2anc	$⊢ (I \in V \land R \in Ring) \to P \in LMod$

Metamath Proof Explorer