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=BaseS
Assertion scmfsupp ⊢M∈LMod∧V∈𝒫BaseM∧A∈RV∧finSupp0S⁡A→finSupp0M⁡v∈V⟼A⁡v⋅Mv

Proof

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