Theorem scmsuppss

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
Hypotheses	scmsuppss.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
	scmsuppss.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
Assertion	scmsuppss	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		scmsuppss.s	⊢ 𝑆 = ( Scalar ‘ 𝑀 )
2		scmsuppss.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
3		elmapi	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
4		fdm	⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → dom 𝐴 = 𝑉 )
5		eqidd	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
6		fveq2	⊢ ( 𝑣 = 𝑥 → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑥 ) )
7		id	⊢ ( 𝑣 = 𝑥 → 𝑣 = 𝑥 )
8	6 7	oveq12d	⊢ ( 𝑣 = 𝑥 → ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
9	8	adantl	⊢ ( ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ 𝑣 = 𝑥 ) → ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
10		simpr	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
11		ovex	⊢ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ V
12	11	a1i	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ∈ V )
13	5 9 10 12	fvmptd	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) = ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
14	13	neeq1d	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ↔ ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ≠ ( 0g ‘ 𝑀 ) ) )
15		oveq1	⊢ ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑆 ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) )
16		simplrr	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑀 ∈ LMod )
17		elelpwi	⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
18	17	expcom	⊢ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
19	18	adantr	⊢ ( ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
20	19	adantl	⊢ ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) → ( 𝑥 ∈ 𝑉 → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
21	20	imp	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) )
22		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
23		eqid	⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
24		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
25		eqid	⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
26	22 1 23 24 25	lmod0vs	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
27	16 21 26	syl2anc	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 0g ‘ 𝑆 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
28	15 27	sylan9eqr	⊢ ( ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑆 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
29	28	ex	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑥 ) = ( 0g ‘ 𝑆 ) → ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) ) )
30	29	necon3d	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝐴 ‘ 𝑥 ) ( ·𝑠 ‘ 𝑀 ) 𝑥 ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) ) )
31	14 30	sylbid	⊢ ( ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) ) )
32	31	ss2rabdv	⊢ ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) → { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
33		ovex	⊢ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ∈ V
34		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
35	33 34	dmmpti	⊢ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = 𝑉
36		rabeq	⊢ ( dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = 𝑉 → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
37	35 36	mp1i	⊢ ( dom 𝐴 = 𝑉 → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
38		rabeq	⊢ ( dom 𝐴 = 𝑉 → { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } = { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
39	37 38	sseq12d	⊢ ( dom 𝐴 = 𝑉 → ( { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ↔ { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) )
40	39	adantr	⊢ ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) → ( { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ↔ { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) )
41	40	adantr	⊢ ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) → ( { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ↔ { 𝑥 ∈ 𝑉 ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ 𝑉 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) )
42	32 41	mpbird	⊢ ( ( ( dom 𝐴 = 𝑉 ∧ 𝐴 : 𝑉 ⟶ 𝑅 ) ∧ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑀 ∈ LMod ) ) → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
43	42	exp43	⊢ ( dom 𝐴 = 𝑉 → ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑀 ∈ LMod → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) ) ) )
44	4 43	mpcom	⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑀 ∈ LMod → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) ) )
45	3 44	syl	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑀 ∈ LMod → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) ) )
46	45	com13	⊢ ( 𝑀 ∈ LMod → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } ) ) )
47	46	3imp	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } ⊆ { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
48		funmpt	⊢ Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
49	48	a1i	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
50		mptexg	⊢ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∈ V )
51	50	3ad2ant2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∈ V )
52		fvexd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 0g ‘ 𝑀 ) ∈ V )
53		suppval1	⊢ ( ( Fun ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∈ V ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
54	49 51 52 53	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑥 ∈ dom ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ∣ ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ‘ 𝑥 ) ≠ ( 0g ‘ 𝑀 ) } )
55		elmapfun	⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → Fun 𝐴 )
56	55	3ad2ant3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → Fun 𝐴 )
57		simp3	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) )
58		fvexd	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 0g ‘ 𝑆 ) ∈ V )
59		suppval1	⊢ ( ( Fun 𝐴 ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑆 ) ∈ V ) → ( 𝐴 supp ( 0g ‘ 𝑆 ) ) = { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
60	56 57 58 59	syl3anc	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐴 supp ( 0g ‘ 𝑆 ) ) = { 𝑥 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( 0g ‘ 𝑆 ) } )
61	47 54 60	3sstr4d	⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐴 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) supp ( 0g ‘ 𝑀 ) ) ⊆ ( 𝐴 supp ( 0g ‘ 𝑆 ) ) )