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\mathrm{mPoly}R$$
	mplrcl.b	$$⊢B={\mathrm{Base}}_P$$
	mplelsfi.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mplelsfi.f	$$⊢\phi \to F\in B$$
	mplelsfi.r	$$⊢\phi \to R\in V$$
Assertion	mplelsfi	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$

Proof

Step	Hyp	Ref	Expression
1		mplrcl.p	$$⊢P=I\mathrm{mPoly}R$$
2		mplrcl.b	$$⊢B={\mathrm{Base}}_P$$
3		mplelsfi.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mplelsfi.f	$$⊢\phi \to F\in B$$
5		mplelsfi.r	$$⊢\phi \to R\in V$$
6		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
7		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
8	1 6 7 3 2	mplelbas	$$⊢F\in B\leftrightarrow \left(F\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
9	8	simprbi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
10	4 9	syl	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$