This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑈 )