Metamath Proof Explorer

Theorem mndpsuppfi

Description: The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019)

		Ref	Expression
	Hypothesis	mndpsuppfi.r	$⊢ R = {Base}_{M}$
	Assertion	mndpsuppfi	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)) \to (A {+_{M}}_{f} B) supp 0_{M} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		mndpsuppfi.r	$⊢ R = {Base}_{M}$
2		unfi	$⊢ (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin) \to {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B) \in Fin$
3	2	3ad2ant3	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)) \to {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B) \in Fin$
4	1	mndpsuppss	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V}))) \to (A {+_{M}}_{f} B) supp 0_{M} \subseteq {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B)$
5	4	3adant3	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)) \to (A {+_{M}}_{f} B) supp 0_{M} \subseteq {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B)$
6		ssfi	$⊢ ({supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B) \in Fin \land (A {+_{M}}_{f} B) supp 0_{M} \subseteq {supp}_{0_{M}} (A) \cup {supp}_{0_{M}} (B)) \to (A {+_{M}}_{f} B) supp 0_{M} \in Fin$
7	3 5 6	syl2anc	$⊢ ((M \in Mnd \land V \in X) \land (A \in (R^{V}) \land B \in (R^{V})) \land (A supp 0_{M} \in Fin \land B supp 0_{M} \in Fin)) \to (A {+_{M}}_{f} B) supp 0_{M} \in Fin$