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 = Base M
Assertion rmfsupp ⊢ M ∈ Ring ∧ V ∈ X ∧ C ∈ R ∧ A ∈ R V ∧ finSupp 0 M⁡ A → finSupp 0 M⁡ v ∈ V ⟼ C ⋅ M A ⁡ v

Proof

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