Metamath Proof Explorer

Theorem rmfsupp

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

Ref Expression
Hypothesis rmsuppfi.r ⊢R=BaseM
Assertion rmfsupp ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→finSupp0M⁡v∈V⟼C⋅MA⁡v

Proof

Step Hyp Ref Expression
1 rmsuppfi.r ⊢R=BaseM
2 funmpt ⊢Fun⁡v∈V⟼C⋅MA⁡v
3 2 a1i ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→Fun⁡v∈V⟼C⋅MA⁡v
4 id ⊢finSupp0M⁡A→finSupp0M⁡A
5 4 fsuppimpd ⊢finSupp0M⁡A→Asupp0M∈Fin
6 1 rmsuppfi ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧Asupp0M∈Fin→v∈V⟼C⋅MA⁡vsupp0M∈Fin
7 5 6 syl3an3 ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→v∈V⟼C⋅MA⁡vsupp0M∈Fin
8 mptexg ⊢V∈X→v∈V⟼C⋅MA⁡v∈V
9 8 3ad2ant2 ⊢M∈Ring∧V∈X∧C∈R→v∈V⟼C⋅MA⁡v∈V
10 9 3ad2ant1 ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→v∈V⟼C⋅MA⁡v∈V
11 fvex ⊢0M∈V
12 isfsupp ⊢v∈V⟼C⋅MA⁡v∈V∧0M∈V→finSupp0M⁡v∈V⟼C⋅MA⁡v↔Fun⁡v∈V⟼C⋅MA⁡v∧v∈V⟼C⋅MA⁡vsupp0M∈Fin
13 10 11 12 sylancl ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→finSupp0M⁡v∈V⟼C⋅MA⁡v↔Fun⁡v∈V⟼C⋅MA⁡v∧v∈V⟼C⋅MA⁡vsupp0M∈Fin
14 3 7 13 mpbir2and ⊢M∈Ring∧V∈X∧C∈R∧A∈RV∧finSupp0M⁡A→finSupp0M⁡v∈V⟼C⋅MA⁡v