Theorem mpllss

Description: The set of polynomials is closed under scalar multiplication, i.e. it is a linear subspace of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Proof shortened by AV, 16-Jul-2019)

	Ref	Expression
Hypotheses	mplsubg.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplsubg.p	$$⊢P=I\mathrm{mPoly}R$$
	mplsubg.u	$$⊢U={\mathrm{Base}}_P$$
	mplsubg.i	$$⊢\phi \to I\in W$$
	mpllss.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mpllss	$$⊢\phi \to U\in \mathrm{LSubSp}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	$$⊢S=I\mathrm{mPwSer}R$$
2		mplsubg.p	$$⊢P=I\mathrm{mPoly}R$$
3		mplsubg.u	$$⊢U={\mathrm{Base}}_P$$
4		mplsubg.i	$$⊢\phi \to I\in W$$
5		mpllss.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
7		eqid	$$⊢0_R=0_R$$
8		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
9		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
10	9	a1i	$$⊢\phi \to \varnothing \in \mathrm{Fin}$$
11		unfi	$$⊢\left(x\in \mathrm{Fin}\wedge y\in \mathrm{Fin}\right)\to x\cup y\in \mathrm{Fin}$$
12	11	adantl	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge y\in \mathrm{Fin}\right)\right)\to x\cup y\in \mathrm{Fin}$$
13		ssfi	$$⊢\left(x\in \mathrm{Fin}\wedge y\subseteq x\right)\to y\in \mathrm{Fin}$$
14	13	adantl	$$⊢\left(\phi \wedge \left(x\in \mathrm{Fin}\wedge y\subseteq x\right)\right)\to y\in \mathrm{Fin}$$
15	1 2 3 4	mplsubglem2	$$⊢\phi \to U=\left\{g\in {\mathrm{Base}}_S|g\mathrm{supp}{0}_R\in \mathrm{Fin}\right\}$$
16	1 6 7 8 4 10 12 14 15 5	mpllsslem	$$⊢\phi \to U\in \mathrm{LSubSp}\left(S\right)$$