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. = ( 0g ` R )
mplbas.u 
|- U = ( Base ` P )
Assertion mplbas 
|- U = { f e. B | f finSupp .0. }

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. = ( 0g ` R )
5 mplbas.u 
 |-  U = ( Base ` P )
6 ssrab2 
 |-  { f e. B | f finSupp .0. } C_ B
7 eqid 
 |-  { f e. B | f finSupp .0. } = { f e. B | f finSupp .0. }
8 1 2 3 4 7 mplval 
 |-  P = ( S |`s { f e. B | f finSupp .0. } )
9 8 3 ressbas2 
 |-  ( { f e. B | f finSupp .0. } C_ B -> { f e. B | f finSupp .0. } = ( Base ` P ) )
10 6 9 ax-mp 
 |-  { f e. B | f finSupp .0. } = ( Base ` P )
11 5 10 eqtr4i 
 |-  U = { f e. B | f finSupp .0. }