Metamath Proof Explorer


Theorem mplelsfi

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 )
Assertion mplelsfi
|- ( ph -> F finSupp .0. )

Proof

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 eqid
 |-  ( I mPwSer R ) = ( I mPwSer R )
6 eqid
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
7 1 5 6 3 2 mplelbas
 |-  ( F e. B <-> ( F e. ( Base ` ( I mPwSer R ) ) /\ F finSupp .0. ) )
8 7 simprbi
 |-  ( F e. B -> F finSupp .0. )
9 4 8 syl
 |-  ( ph -> F finSupp .0. )