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. } |
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. } |