Description: Property of being a polynomial. (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 | mplelbas | |- ( X e. U <-> ( X e. B /\ X 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 | breq1 | |- ( f = X -> ( f finSupp .0. <-> X finSupp .0. ) ) |
|
| 7 | 1 2 3 4 5 | mplbas | |- U = { f e. B | f finSupp .0. } |
| 8 | 6 7 | elrab2 | |- ( X e. U <-> ( X e. B /\ X finSupp .0. ) ) |