Metamath Proof Explorer

Theorem domnmsuppn0

Description: The support of a mapping of a multiplication of a nonzero constant with a function into a (ring theoretic) domain equals the support of the function. (Contributed by AV, 11-Apr-2019)

Ref Expression
Hypothesis rmsuppss.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
Assertion domnmsuppn0 ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = ( 𝐴 supp ( 0g ‘ 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 rmsuppss.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 elmapi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
3 fdm ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → dom 𝐴 = 𝑉 )
4 3 eqcomd ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → 𝑉 = dom 𝐴 )
5 2 4 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑉 = dom 𝐴 )
6 5 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 = dom 𝐴 )
7 oveq2 ⊢ ( ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
8 domnring ⊢ ( 𝑀 ∈ Domn → 𝑀 ∈ Ring )
9 8 adantr ⊢ ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) → 𝑀 ∈ Ring )
10 simpl ⊢ ( ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) → 𝐶 ∈ 𝑅 )
11 9 10 anim12i ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ) → ( 𝑀 ∈ Ring ∧ 𝐶 ∈ 𝑅 ) )
12 11 3adant3 ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑀 ∈ Ring ∧ 𝐶 ∈ 𝑅 ) )
13 eqid ⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
14 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
15 1 13 14 ringrz ⊢ ( ( 𝑀 ∈ Ring ∧ 𝐶 ∈ 𝑅 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
16 12 15 syl ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
17 16 adantr ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( 0g ‘ 𝑀 ) )
18 7 17 sylan9eqr ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) )
19 18 ex ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑤 ) = ( 0g ‘ 𝑀 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) ) )
20 19 necon3d ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) )
21 simpl1l ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝑀 ∈ Domn )
22 21 adantr ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) → 𝑀 ∈ Domn )
23 simpll2 ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) → ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) )
24 ffvelrn ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑤 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 )
25 24 ex ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 ) )
26 2 25 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 ) )
27 26 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 ) )
28 27 imp ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 )
29 28 adantr ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 )
30 simpr ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) → ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) )
31 1 13 14 domnmuln0 ⊢ ( ( 𝑀 ∈ Domn ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ ( ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) )
32 22 23 29 30 31 syl112anc ⊢ ( ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) ∧ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) )
33 32 ex ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) ) )
34 20 33 impbid ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) ) )
35 6 34 rabeqbidva ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
36 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑤 ) )
37 36 oveq2d ⊢ ( 𝑣 = 𝑤 → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) = ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
38 37 cbvmptv ⊢ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑤 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
39 simp1r ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 ∈ 𝑋 )
40 fvexd ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 0g ‘ 𝑀 ) ∈ V )
41 ovexd ⊢ ( ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ∈ V )
42 38 39 40 41 mptsuppd ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } )
43 elmapfun ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → Fun 𝐴 )
44 43 3ad2ant3 ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → Fun 𝐴 )
45 simp3 ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) )
46 suppval1 ⊢ ( ( Fun 𝐴 ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ∧ ( 0g ‘ 𝑀 ) ∈ V ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
47 44 45 40 46 syl3anc ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝐴 supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ dom 𝐴 ∣ ( 𝐴 ‘ 𝑤 ) ≠ ( 0g ‘ 𝑀 ) } )
48 35 42 47 3eqtr4d ⊢ ( ( ( 𝑀 ∈ Domn ∧ 𝑉 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐶 ≠ ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = ( 𝐴 supp ( 0g ‘ 𝑀 ) ) )