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

Metamath Proof Explorer

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 ⊢ P = I mPoly R
mplval.s ⊢ S = I mPwSer R
mplval.b ⊢ B = Base S
mplval.z ⊢ 0 ˙ = 0 R
mplbas.u ⊢ U = Base P
Assertion mplbas ⊢ U = f ∈ B | finSupp 0 ˙⁡ f

Proof

Step Hyp Ref Expression
1 mplval.p ⊢ P = I mPoly R
2 mplval.s ⊢ S = I mPwSer R
3 mplval.b ⊢ B = Base S
4 mplval.z ⊢ 0 ˙ = 0 R
5 mplbas.u ⊢ U = Base P
6 ssrab2 ⊢ f ∈ B | finSupp 0 ˙⁡ f ⊆ B
7 eqid ⊢ f ∈ B | finSupp 0 ˙⁡ f = f ∈ B | finSupp 0 ˙⁡ f
8 1 2 3 4 7 mplval ⊢ P = S ↾ 𝑠 f ∈ B | finSupp 0 ˙⁡ f
9 8 3 ressbas2 ⊢ f ∈ B | finSupp 0 ˙⁡ f ⊆ B → f ∈ B | finSupp 0 ˙⁡ f = Base P
10 6 9 ax-mp ⊢ f ∈ B | finSupp 0 ˙⁡ f = Base P
11 5 10 eqtr4i ⊢ U = f ∈ B | finSupp 0 ˙⁡ f