Metamath Proof Explorer

Theorem scmsuppfi

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
	Hypotheses	scmsuppfi.s	$⊢ S = Scalar (M)$
		scmsuppfi.r	$⊢ R = {Base}_{S}$
	Assertion	scmsuppfi	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land A supp 0_{S} \in Fin) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		scmsuppfi.s	$⊢ S = Scalar (M)$
2		scmsuppfi.r	$⊢ R = {Base}_{S}$
3		simp3	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land A supp 0_{S} \in Fin) \to A supp 0_{S} \in Fin$
4		simpll	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V})) \to M \in LMod$
5		simplr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V})) \to V \in 𝒫 {Base}_{M}$
6		simpr	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V})) \to A \in (R^{V})$
7	4 5 6	3jca	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V})) \to (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V}))$
8	7	3adant3	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land A supp 0_{S} \in Fin) \to (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V}))$
9	1 2	scmsuppss	$⊢ (M \in LMod \land V \in 𝒫 {Base}_{M} \land A \in (R^{V})) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \subseteq A supp 0_{S}$
10	8 9	syl	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land A supp 0_{S} \in Fin) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \subseteq A supp 0_{S}$
11		ssfi	$⊢ (A supp 0_{S} \in Fin \land (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \subseteq A supp 0_{S}) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \in Fin$
12	3 10 11	syl2anc	$⊢ ((M \in LMod \land V \in 𝒫 {Base}_{M}) \land A \in (R^{V}) \land A supp 0_{S} \in Fin) \to (v \in V ⟼ A (v) \cdot_{M} v) supp 0_{M} \in Fin$