Metamath Proof Explorer

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