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 ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin

Proof

Step Hyp Ref Expression
1 scmsuppfi.s ⊢ S = Scalar ⁡ M
2 scmsuppfi.r ⊢ R = Base S
3 simp3 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → A supp 0 S ∈ Fin
4 simpll ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V → M ∈ LMod
5 simplr ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V → V ∈ 𝒫 Base M
6 simpr ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V → A ∈ R V
7 4 5 6 3jca ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V → M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V
8 7 3adant3 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V
9 1 2 scmsuppss ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ⊆ A supp 0 S
10 8 9 syl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ⊆ A supp 0 S
11 ssfi ⊢ A supp 0 S ∈ Fin ∧ v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ⊆ A supp 0 S → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin
12 3 10 11 syl2anc ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin