Theorem mplval2

Description: Self-referential expression for the set of multivariate polynomials. (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 )
Assertion	mplval2	|- P = ( S |`s U )

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		eqid	|- ( Base ` S ) = ( Base ` S )
5		eqid	|- ( 0g ` R ) = ( 0g ` R )
6	1 2 4 5 3	mplbas	|- U = { f e. ( Base ` S ) | f finSupp ( 0g ` R ) }
7	1 2 4 5 6	mplval	|- P = ( S |`s U )