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

Metamath Proof Explorer

Theorem mndpsuppss

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

Ref Expression
Hypothesis mndpsuppss.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
Assertion mndpsuppss ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) )

Proof

Step Hyp Ref Expression
1 mndpsuppss.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 ioran ⊢ ( ¬ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) ↔ ( ¬ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∧ ¬ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) )
3 nne ⊢ ( ¬ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
4 nne ⊢ ( ¬ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
5 3 4 anbi12i ⊢ ( ( ¬ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∧ ¬ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) ↔ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) )
6 2 5 bitri ⊢ ( ¬ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) ↔ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) )
7 elmapfn ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 Fn 𝑉 )
8 7 ad2antrl ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐴 Fn 𝑉 )
9 8 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → 𝐴 Fn 𝑉 )
10 elmapfn ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 Fn 𝑉 )
11 10 ad2antll ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 Fn 𝑉 )
12 11 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → 𝐵 Fn 𝑉 )
13 simplr ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝑉 ∈ 𝑋 )
14 13 adantr ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → 𝑉 ∈ 𝑋 )
15 inidm ⊢ ( 𝑉 ∩ 𝑉 ) = 𝑉
16 simplrl ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
17 simplrr ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
18 9 12 14 14 15 16 17 ofval ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
19 18 an32s ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
20 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
21 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
22 20 21 mndidcl ⊢ ( 𝑀 ∈ Mnd → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
23 22 ancli ⊢ ( 𝑀 ∈ Mnd → ( 𝑀 ∈ Mnd ∧ ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ) )
24 23 ad4antr ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → ( 𝑀 ∈ Mnd ∧ ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ) )
25 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
26 20 25 21 mndlid ⊢ ( ( 𝑀 ∈ Mnd ∧ ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
27 24 26 syl ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
28 19 27 eqtrd ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
29 nne ⊢ ( ¬ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) )
30 28 29 sylibr ⊢ ( ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) ) → ¬ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) )
31 30 ex ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ∧ ( 𝐵 ‘ 𝑥 ) = ( 0g ‘ 𝑀 ) ) → ¬ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) )
32 6 31 biimtrid ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ¬ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) → ¬ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) )
33 32 con4d ⊢ ( ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) → ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) ) )
34 33 ss2rabdv ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) } )
35 8 11 13 13 offun ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → Fun ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) )
36 ovexd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∈ V )
37 fvexd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 0g ‘ 𝑀 ) ∈ V )
38 suppval1 ⊢ ( ( Fun ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∧ ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
39 35 36 37 38 syl3anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
40 13 8 11 offvalfv ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) ) )
41 40 dmeqd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → dom ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) = dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) ) )
42 ovex ⊢ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) ∈ V
43 eqid ⊢ ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) )
44 42 43 dmmpti ⊢ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( +g ‘ 𝑀 ) ( 𝐵 ‘ 𝑣 ) ) ) = 𝑉
45 41 44 eqtrdi ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → dom ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) = 𝑉 )
46 45 rabeqdv ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → { 𝑥 ∈ dom ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
47 39 46 eqtrd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
48 elmapfun ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → Fun 𝐴 )
49 id ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) )
50 fvexd ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 0g ‘ 𝑀 ) ∈ V )
51 suppval1 ⊢ ( ( Fun 𝐴 ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
52 48 49 50 51 syl3anc ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
53 elmapi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
54 fdm ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → dom 𝐴 = 𝑉 )
55 rabeq ⊢ ( dom 𝐴 = 𝑉 → { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
56 53 54 55 3syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
57 52 56 eqtrd ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
58 57 ad2antrl ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
59 elmapfun ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → Fun 𝐵 )
60 59 ad2antll ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → Fun 𝐵 )
61 simprr ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) )
62 suppval1 ⊢ ( ( Fun 𝐵 ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( 𝐵 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom 𝐵 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
63 60 61 37 62 syl3anc ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐵 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom 𝐵 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
64 elmapi ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐵 : 𝑉 ⟶ 𝑅 )
65 64 fdmd ⊢ ( 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) → dom 𝐵 = 𝑉 )
66 65 ad2antll ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → dom 𝐵 = 𝑉 )
67 66 rabeqdv ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → { 𝑥 ∈ dom 𝐵 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
68 63 67 eqtrd ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝐵 supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ 𝑉 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
69 58 68 uneq12d ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) = ( { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ∪ { 𝑥 ∈ 𝑉 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ) )
70 unrab ⊢ ( { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ∪ { 𝑥 ∈ 𝑉 ∣ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ) = { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) }
71 69 70 eqtrdi ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) = { 𝑥 ∈ 𝑉 ∣ ( ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ∨ ( 𝐵 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) } )
72 34 47 71 3sstr4d ⊢ ( ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝐵 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝐴 ∘f ( +g ‘ 𝑀 ) 𝐵 ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( ( 𝐴 supp ( 0g ‘ 𝑀 ) ) ∪ ( 𝐵 supp ( 0g ‘ 𝑀 ) ) ) )