Theorem mplbas

Description: Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015) (Revised by Mario Carneiro, 2-Oct-2015) (Revised by AV, 25-Jun-2019)

	Ref	Expression
Hypotheses	mplval.p	|- P = ( I mPoly R )
	mplval.s	|- S = ( I mPwSer R )
	mplval.b	|- B = ( Base ` S )
	mplval.z	|- .0. = ( 0g ` R )
	mplbas.u	|- U = ( Base ` P )
Assertion	mplbas	|- U = { f e. B | f finSupp .0. }

Proof

Step	Hyp	Ref	Expression
1		mplval.p	|- P = ( I mPoly R )
2		mplval.s	|- S = ( I mPwSer R )
3		mplval.b	|- B = ( Base ` S )
4		mplval.z	|- .0. = ( 0g ` R )
5		mplbas.u	|- U = ( Base ` P )
6		ssrab2	|- { f e. B | f finSupp .0. } C_ B
7		eqid	|- { f e. B | f finSupp .0. } = { f e. B | f finSupp .0. }
8	1 2 3 4 7	mplval	|- P = ( S |`s { f e. B | f finSupp .0. } )
9	8 3	ressbas2	|- ( { f e. B | f finSupp .0. } C_ B -> { f e. B | f finSupp .0. } = ( Base ` P ) )
10	6 9	ax-mp	|- { f e. B | f finSupp .0. } = ( Base ` P )
11	5 10	eqtr4i	|- U = { f e. B | f finSupp .0. }