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 mPoly R )
	mplval2.s	|- S = ( I mPwSer R )
	mplval2.u	|- U = ( Base ` P )
	mplbasss.b	|- B = ( Base ` S )
Assertion	mplbasss	|- U C_ B

Proof

Step	Hyp	Ref	Expression
1		mplval2.p	|- P = ( I mPoly R )
2		mplval2.s	|- S = ( I mPwSer R )
3		mplval2.u	|- U = ( Base ` P )
4		mplbasss.b	|- B = ( Base ` S )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6	1 2 4 5 3	mplbas	|- U = { f e. B | f finSupp ( 0g ` R ) }
7	6	ssrab3	|- U C_ B