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 ‘ 𝑀 ) ) ) )