This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mndpsuppfi

Description: The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019)

Ref Expression
Hypothesis mndpsuppfi.r ⊢ R = Base M
Assertion 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

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r ⊢ R = Base M
2 unfi ⊢ A supp 0 M ∈ Fin ∧ B supp 0 M ∈ Fin → supp 0 M⁡ A ∪ supp 0 M⁡ B ∈ Fin
3 2 3ad2ant3 ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V ∧ A supp 0 M ∈ Fin ∧ B supp 0 M ∈ Fin → supp 0 M⁡ A ∪ supp 0 M⁡ B ∈ Fin
4 1 mndpsuppss ⊢ M ∈ Mnd ∧ V ∈ X ∧ A ∈ R V ∧ B ∈ R V → A + M f B supp 0 M ⊆ supp 0 M⁡ A ∪ supp 0 M⁡ B
5 4 3adant3 ⊢ 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 ⊆ supp 0 M⁡ A ∪ supp 0 M⁡ B
6 ssfi ⊢ supp 0 M⁡ A ∪ supp 0 M⁡ B ∈ Fin ∧ A + M f B supp 0 M ⊆ supp 0 M⁡ A ∪ supp 0 M⁡ B → A + M f B supp 0 M ∈ Fin
7 3 5 6 syl2anc ⊢ 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