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

Proof

Step Hyp Ref Expression
1 mndpsuppfi.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 elmapfn ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 Fn 𝑉 )
3 2 adantr ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 Fn 𝑉 )
4 3 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → 𝐴 Fn 𝑉 )
5 elmapfn ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 Fn 𝑉 )
6 5 adantl ⊢ ( ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐵 Fn 𝑉 )
7 6 3ad2ant2 ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → 𝐵 Fn 𝑉 )
8 simp1r ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → 𝑉 ∈ 𝑋 )
9 4 7 8 8 offun ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → Fun ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) )
10 id ⊢ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) → 𝐴 finSupp ( 0g ‘ 𝑀 ) )
11 10 fsuppimpd ⊢ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
12 id ⊢ ( 𝐵 finSupp ( 0g ‘ 𝑀 ) → 𝐵 finSupp ( 0g ‘ 𝑀 ) )
13 12 fsuppimpd ⊢ ( 𝐵 finSupp ( 0g ‘ 𝑀 ) → ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
14 11 13 anim12i ⊢ ( ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) → ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) )
15 1 mndpsuppfi ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ∧ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
16 14 15 syl3an3 ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin )
17 ovex ⊢ ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∈ V
18 fvexd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → ( 0g ‘ 𝑀 ) ∈ V )
19 isfsupp ⊢ ( ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∧ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) )
20 17 18 19 sylancr ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) finSupp ( 0g ‘ 𝑀 ) ↔ ( Fun ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∧ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ∈ Fin ) ) )
21 9 16 20 mpbir2and ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ ( 𝐴 finSupp ( 0g ‘ 𝑀 ) ∧ 𝐵 finSupp ( 0g ‘ 𝑀 ) ) ) → ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) finSupp ( 0g ‘ 𝑀 ) )