ply1lmod

Description: Univariate polynomials form a left module. (Contributed by Stefan O'Rear, 26-Mar-2015)

		Ref	Expression
	Hypothesis	ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
	Assertion	ply1lmod	$⊢ R \in Ring \to P \in LMod$

Step	Hyp	Ref	Expression
1		ply1lmod.p	$⊢ P = {Poly}_{1} (R)$
2		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
3	2	psr1lmod	$⊢ R \in Ring \to {PwSer}_{1} (R) \in LMod$
4		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
5		eqid	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{{Poly}_{1} (R)}$
6	4 5	ply1bas	$⊢ {Base}_{{Poly}_{1} (R)} = {Base}_{(1_{𝑜} mPoly R)}$
7	4 2 5	ply1lss	$⊢ R \in Ring \to {Base}_{{Poly}_{1} (R)} \in LSubSp ({PwSer}_{1} (R))$
8	6 7	eqeltrrid	$⊢ R \in Ring \to {Base}_{(1_{𝑜} mPoly R)} \in LSubSp ({PwSer}_{1} (R))$
9	1 2	ply1val	$⊢ P = {PwSer}_{1} (R) ↾_{𝑠} {Base}_{(1_{𝑜} mPoly R)}$
10		eqid	$⊢ LSubSp ({PwSer}_{1} (R)) = LSubSp ({PwSer}_{1} (R))$
11	9 10	lsslmod	$⊢ ({PwSer}_{1} (R) \in LMod \land {Base}_{(1_{𝑜} mPoly R)} \in LSubSp ({PwSer}_{1} (R))) \to P \in LMod$
12	3 8 11	syl2anc	$⊢ R \in Ring \to P \in LMod$

Metamath Proof Explorer