This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \subseteq 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	$⊢ 0_{R} = 0_{R}$
6	1 2 4 5 3	mplbas	$⊢ U = \{f \in B \| {finSupp}_{0_{R}} (f)\}$
7	6	ssrab3	$⊢ U \subseteq B$