Theorem mplelbas

Description: Property of being a polynomial. (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	mplelbas	$$⊢X\in U\leftrightarrow \left(X\in B\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\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		breq1	$$⊢f=X\to \left({finSupp}_{\underset{\dot{}}{0}}\left(f\right)\leftrightarrow {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$
7	1 2 3 4 5	mplbas	$$⊢U=\left\{f\in B|{finSupp}_{\underset{\dot{}}{0}}\left(f\right)\right\}$$
8	6 7	elrab2	$$⊢X\in U\leftrightarrow \left(X\in B\wedge {finSupp}_{\underset{\dot{}}{0}}\left(X\right)\right)$$