Metamath Proof Explorer

Theorem mndpfsupp

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
Hypothesis mndpsuppfi.r ⊢ R = Base M
Assertion mndpfsupp ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → finSupp 0 M⁡ A + M f B

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r ⊢ R = Base M
2 elmapfn ⊢ A ∈ R V → A Fn V
3 2 adantr ⊢ A ∈ R V ∧ B ∈ R V → A Fn V
4 3 3ad2ant2 ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → A Fn V
5 elmapfn ⊢ B ∈ R V → B Fn V
6 5 adantl ⊢ A ∈ R V ∧ B ∈ R V → B Fn V
7 6 3ad2ant2 ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → B Fn V
8 simp1r ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → V ∈ X
9 4 7 8 8 offun ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → Fun ⁡ A + M f B
10 id ⊢ finSupp 0 M⁡ A → finSupp 0 M⁡ A
11 10 fsuppimpd ⊢ finSupp 0 M⁡ A → A supp 0 M ∈ Fin
12 id ⊢ finSupp 0 M⁡ B → finSupp 0 M⁡ B
13 12 fsuppimpd ⊢ finSupp 0 M⁡ B → B supp 0 M ∈ Fin
14 11 13 anim12i ⊢ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → A supp 0 M ∈ Fin ∧ B supp 0 M ∈ Fin
15 1 mndpsuppfi ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ A supp 0 M ∈ Fin ∧ B supp 0 M ∈ Fin → A + M f B supp 0 M ∈ Fin
16 14 15 syl3an3 ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → A + M f B supp 0 M ∈ Fin
17 ovex ⊢ A + M f B ∈ V
18 fvexd ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → 0 M ∈ V
19 isfsupp ⊢ A + M f B ∈ V ∧ 0 M ∈ V → finSupp 0 M⁡ A + M f B ↔ Fun ⁡ A + M f B ∧ A + M f B supp 0 M ∈ Fin
20 17 18 19 sylancr ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → finSupp 0 M⁡ A + M f B ↔ Fun ⁡ A + M f B ∧ A + M f B supp 0 M ∈ Fin
21 9 16 20 mpbir2and ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ finSupp 0 M⁡ A ∧ finSupp 0 M⁡ B → finSupp 0 M⁡ A + M f B