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$$
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		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
6		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
7	1 5 6 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)$$
8	7	simprbi	$$⊢F\in B\to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
9	4 8	syl	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$