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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplval.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	mplval.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplbas.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
Assertion	mplbas	⊢ 𝑈 = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }

Proof

Step	Hyp	Ref	Expression
1		mplval.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplval.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
3		mplval.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
4		mplval.z	⊢ 0 = ( 0g ‘ 𝑅 )
5		mplbas.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
6		ssrab2	⊢ { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } ⊆ 𝐵
7		eqid	⊢ { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }
8	1 2 3 4 7	mplval	⊢ 𝑃 = ( 𝑆 ↾s { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } )
9	8 3	ressbas2	⊢ ( { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } ⊆ 𝐵 → { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } = ( Base ‘ 𝑃 ) )
10	6 9	ax-mp	⊢ { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 } = ( Base ‘ 𝑃 )
11	5 10	eqtr4i	⊢ 𝑈 = { 𝑓 ∈ 𝐵 ∣ 𝑓 finSupp 0 }