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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplval2.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplval2.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
Assertion	mplval2	⊢ 𝑃 = ( 𝑆 ↾s 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mplval2.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplval2.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3		mplval2.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
5		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
6	1 2 4 5 3	mplbas	⊢ 𝑈 = { 𝑓 ∈ ( Base ‘ 𝑆 ) ∣ 𝑓 finSupp ( 0g ‘ 𝑅 ) }
7	1 2 4 5 6	mplval	⊢ 𝑃 = ( 𝑆 ↾s 𝑈 )