Theorem ply1lmod

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

	Ref	Expression
Hypothesis	ply1lmod.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$

Proof

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