Theorem ply1lss

Description: Univariate polynomials form a linear subspace of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1lss.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
	ply1lss.u	$$⊢U={\mathrm{Base}}_P$$
Assertion	ply1lss	$$⊢R\in \mathrm{Ring}\to U\in \mathrm{LSubSp}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1lss.2	$$⊢S={\mathrm{PwSer}}_1\left(R\right)$$
3		ply1lss.u	$$⊢U={\mathrm{Base}}_P$$
4		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
6	1 3	ply1bas	$$⊢U={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
7		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
8	7	a1i	$$⊢R\in \mathrm{Ring}\to 1_{𝑜}\in \mathrm{On}$$
9		id	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
10	4 5 6 8 9	mpllss	$$⊢R\in \mathrm{Ring}\to U\in \mathrm{LSubSp}\left(1_{𝑜}\mathrm{mPwSer}R\right)$$
11		eqidd	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
12	2	psr1val	$$⊢S=\left(1_{𝑜}\mathrm{ordPwSer}R\right)\left(\varnothing \right)$$
13		0ss	$$⊢\varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
14	13	a1i	$$⊢R\in \mathrm{Ring}\to \varnothing \subseteq 1_{𝑜}\times 1_{𝑜}$$
15	4 12 14	opsrbas	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_S$$
16		ssv	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\subseteq \mathrm{V}$$
17	16	a1i	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\subseteq \mathrm{V}$$
18	4 12 14	opsrplusg	$$⊢R\in \mathrm{Ring}\to {+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={+}_S$$
19	18	oveqdr	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\right)\to x{+}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}y=x{+}_{S}y$$
20		ovexd	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\right)\right)\to x{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}y\in \mathrm{V}$$
21	4 12 14	opsrvsca	$$⊢R\in \mathrm{Ring}\to {\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\cdot }_S$$
22	21	oveqdr	$$⊢\left(R\in \mathrm{Ring}\wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\right)\right)\to x{\cdot }_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}y=x{\cdot }_{S}y$$
23	4 8 9	psrsca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPwSer}R\right)$$
24	23	fveq2d	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
25	4 12 14 8 9	opsrsca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(S\right)$$
26	25	fveq2d	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(S\right)}$$
27	11 15 17 19 20 22 24 26	lsspropd	$$⊢R\in \mathrm{Ring}\to \mathrm{LSubSp}\left(1_{𝑜}\mathrm{mPwSer}R\right)=\mathrm{LSubSp}\left(S\right)$$
28	10 27	eleqtrd	$$⊢R\in \mathrm{Ring}\to U\in \mathrm{LSubSp}\left(S\right)$$