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	$⊢ P = I mPoly R$
		mplrcl.b	$⊢ B = {Base}_{P}$
		mplelsfi.z	$⊢ \underset{˙}{0} = 0_{R}$
		mplelsfi.f	$⊢ φ \to F \in B$
	Assertion	mplelsfi	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$

Proof

Step	Hyp	Ref	Expression
1		mplrcl.p	$⊢ P = I mPoly R$
2		mplrcl.b	$⊢ B = {Base}_{P}$
3		mplelsfi.z	$⊢ \underset{˙}{0} = 0_{R}$
4		mplelsfi.f	$⊢ φ \to F \in 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 \in B \leftrightarrow (F \in {Base}_{(I mPwSer R)} \land {finSupp}_{\underset{˙}{0}} (F))$
8	7	simprbi	$⊢ F \in B \to {finSupp}_{\underset{˙}{0}} (F)$
9	4 8	syl	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (F)$