Theorem mplbasss

Description: The set of polynomials is a subset of the set of power series. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	mplval2.p	$$⊢P=I\mathrm{mPoly}R$$
	mplval2.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplval2.u	$$⊢U={\mathrm{Base}}_P$$
	mplbasss.b	$$⊢B={\mathrm{Base}}_S$$
Assertion	mplbasss	$$⊢U\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		mplval2.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplval2.s	$$⊢S=I\mathrm{mPwSer}R$$
3		mplval2.u	$$⊢U={\mathrm{Base}}_P$$
4		mplbasss.b	$$⊢B={\mathrm{Base}}_S$$
5		eqid	$$⊢0_R=0_R$$
6	1 2 4 5 3	mplbas	$$⊢U=\left\{f\in B|{finSupp}_{0_R}\left(f\right)\right\}$$
7	6	ssrab3	$$⊢U\subseteq B$$