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 )