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\mathrm{mPoly}R$$
	mplval2.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplval2.u	$$⊢U={\mathrm{Base}}_P$$
Assertion	mplval2	$$⊢P=S{\upharpoonright }_{𝑠}U$$

Proof

Step	Hyp	Ref	Expression
1		mplval2.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplval2.s	$$⊢S=I\mathrm{mPwSer}R$$
3		mplval2.u	$$⊢U={\mathrm{Base}}_P$$
4		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
5		eqid	$$⊢0_R=0_R$$
6	1 2 4 5 3	mplbas	$$⊢U=\left\{f\in {\mathrm{Base}}_S|{finSupp}_{0_R}\left(f\right)\right\}$$
7	1 2 4 5 6	mplval	$$⊢P=S{\upharpoonright }_{𝑠}U$$