# Metamath Proof Explorer

## 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)$
ply1val.2 ${⊢}{S}={\mathrm{PwSer}}_{1}\left({R}\right)$
ply1bas.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 ply1val.2 ${⊢}{S}={\mathrm{PwSer}}_{1}\left({R}\right)$
3 ply1bas.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 2 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}_{𝑜}×{1}_{𝑜}$
14 13 a1i ${⊢}{R}\in \mathrm{Ring}\to \varnothing \subseteq {1}_{𝑜}×{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)$