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 ⊢ 𝑅 = ( Base ‘ 𝑀 )
Assertion mndpsuppfi ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 unfi ⊢ ( ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) → ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) ∈ Fin )
3 2 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) → ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) ∈ Fin )
4 1 mndpsuppss ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) )
5 4 3adant3 ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) )
6 ssfi ⊢ ( ( ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) ∈ Fin ∧ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
7 3 5 6 syl2anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )