This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
mplelsfi.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplelsfi.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion mplelsfi ( 𝜑 → 𝐹 finSupp 0 )

Proof

Step Hyp Ref Expression
1 mplrcl.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplrcl.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 mplelsfi.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplelsfi.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
5 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6 eqid ⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
7 1 5 6 3 2 mplelbas ⊢ ( 𝐹 ∈ 𝐵 ↔ ( 𝐹 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝐹 finSupp 0 ) )
8 7 simprbi ⊢ ( 𝐹 ∈ 𝐵 → 𝐹 finSupp 0 )
9 4 8 syl ⊢ ( 𝜑 → 𝐹 finSupp 0 )