Metamath Proof Explorer

Theorem scmfsupp

Description: A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019)

Ref Expression
Hypotheses scmsuppfi.s ⊢ S = Scalar ⁡ M
scmsuppfi.r ⊢ R = Base S
Assertion scmfsupp ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → finSupp 0 M⁡ v ∈ V ⟼ A ⁡ v ⋅ M v

Proof

Step Hyp Ref Expression
1 scmsuppfi.s ⊢ S = Scalar ⁡ M
2 scmsuppfi.r ⊢ R = Base S
3 funmpt ⊢ Fun ⁡ v ∈ V ⟼ A ⁡ v ⋅ M v
4 3 a1i ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → Fun ⁡ v ∈ V ⟼ A ⁡ v ⋅ M v
5 id ⊢ finSupp 0 S⁡ A → finSupp 0 S⁡ A
6 5 fsuppimpd ⊢ finSupp 0 S⁡ A → A supp 0 S ∈ Fin
7 1 2 scmsuppfi ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ A supp 0 S ∈ Fin → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin
8 6 7 syl3an3 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin
9 mptexg ⊢ V ∈ 𝒫 Base M → v ∈ V ⟼ A ⁡ v ⋅ M v ∈ V
10 9 adantl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M → v ∈ V ⟼ A ⁡ v ⋅ M v ∈ V
11 10 3ad2ant1 ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → v ∈ V ⟼ A ⁡ v ⋅ M v ∈ V
12 fvex ⊢ 0 M ∈ V
13 isfsupp ⊢ v ∈ V ⟼ A ⁡ v ⋅ M v ∈ V ∧ 0 M ∈ V → finSupp 0 M⁡ v ∈ V ⟼ A ⁡ v ⋅ M v ↔ Fun ⁡ v ∈ V ⟼ A ⁡ v ⋅ M v ∧ v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin
14 11 12 13 sylancl ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → finSupp 0 M⁡ v ∈ V ⟼ A ⁡ v ⋅ M v ↔ Fun ⁡ v ∈ V ⟼ A ⁡ v ⋅ M v ∧ v ∈ V ⟼ A ⁡ v ⋅ M v supp 0 M ∈ Fin
15 4 8 14 mpbir2and ⊢ M ∈ LMod ∧ V ∈ 𝒫 Base M ∧ A ∈ R V ∧ finSupp 0 S⁡ A → finSupp 0 M⁡ v ∈ V ⟼ A ⁡ v ⋅ M v