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\mathrm{mPoly}R$$
	mplval.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplval.b	$$⊢B={\mathrm{Base}}_S$$
	mplval.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplbas.u	$$⊢U={\mathrm{Base}}_P$$
Assertion	mplbas	$$⊢U=\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mplval.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplval.s	$$⊢S=I\mathrm{mPwSer}R$$
3		mplval.b	$$⊢B={\mathrm{Base}}_S$$
4		mplval.z	$$⊢\underset{\dot{}}{0}=0_R$$
5		mplbas.u	$$⊢U={\mathrm{Base}}_P$$
6		ssrab2	$$⊢\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}\subseteq B$$
7		eqid	$$⊢\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}=\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}$$
8	1 2 3 4 7	mplval	$$⊢P=S{\upharpoonright }_{𝑠}\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}$$
9	8 3	ressbas2	$$⊢\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}\subseteq B\to \left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}={\mathrm{Base}}_P$$
10	6 9	ax-mp	$$⊢\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}={\mathrm{Base}}_P$$
11	5 10	eqtr4i	$$⊢U=\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}$$