Description: A polynomial treated as a coefficient function has finitely many nonzero terms. (Contributed by Stefan O'Rear, 22-Mar-2015) (Revised by AV, 25-Jun-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mplrcl.p | |- P = ( I mPoly R ) |
|
| mplrcl.b | |- B = ( Base ` P ) |
||
| mplelsfi.z | |- .0. = ( 0g ` R ) |
||
| mplelsfi.f | |- ( ph -> F e. B ) |
||
| mplelsfi.r | |- ( ph -> R e. V ) |
||
| Assertion | mplelsfi | |- ( ph -> F finSupp .0. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mplrcl.p | |- P = ( I mPoly R ) |
|
| 2 | mplrcl.b | |- B = ( Base ` P ) |
|
| 3 | mplelsfi.z | |- .0. = ( 0g ` R ) |
|
| 4 | mplelsfi.f | |- ( ph -> F e. B ) |
|
| 5 | mplelsfi.r | |- ( ph -> R e. V ) |
|
| 6 | eqid | |- ( I mPwSer R ) = ( I mPwSer R ) |
|
| 7 | eqid | |- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) |
|
| 8 | 1 6 7 3 2 | mplelbas | |- ( F e. B <-> ( F e. ( Base ` ( I mPwSer R ) ) /\ F finSupp .0. ) ) |
| 9 | 8 | simprbi | |- ( F e. B -> F finSupp .0. ) |
| 10 | 4 9 | syl | |- ( ph -> F finSupp .0. ) |