Metamath Proof Explorer

Theorem rmsupp0

Description: The support of a mapping of a multiplication of zero with a function into a ring is empty. (Contributed by AV, 10-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 rmsuppss.r ⊢ 𝑅 = ( Base ‘ 𝑀 )
2 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐴 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑤 ) )
3 2 oveq2d ⊢ ( 𝑣 = 𝑤 → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) = ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
4 3 cbvmptv ⊢ ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) = ( 𝑤 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
5 simpl2 ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → 𝑉 ∈ 𝑋 )
6 fvexd ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 0g ‘ 𝑀 ) ∈ V )
7 ovexd ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ∈ V )
8 4 5 6 7 mptsuppd ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } )
9 simpll3 ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝐶 = ( 0g ‘ 𝑀 ) )
10 9 oveq1d ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) )
11 simpll1 ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → 𝑀 ∈ Ring )
12 elmapi ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → 𝐴 : 𝑉 ⟶ 𝑅 )
13 ffvelcdm ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑤 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑤 ) ∈ 𝑅 )
14 13 1 eleqtrdi ⊢ ( ( 𝐴 : 𝑉 ⟶ 𝑅 ∧ 𝑤 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) )
15 14 ex ⊢ ( 𝐴 : 𝑉 ⟶ 𝑅 → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) ) )
16 12 15 syl ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) ) )
17 16 adantl ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑤 ∈ 𝑉 → ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) ) )
18 17 imp ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) )
19 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
20 eqid ⊢ ( .r ‘ 𝑀 ) = ( .r ‘ 𝑀 )
21 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
22 19 20 21 ringlz ⊢ ( ( 𝑀 ∈ Ring ∧ ( 𝐴 ‘ 𝑤 ) ∈ ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) )
23 11 18 22 syl2anc ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 0g ‘ 𝑀 ) ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) )
24 10 23 eqtrd ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) = ( 0g ‘ 𝑀 ) )
25 24 neeq1d ⊢ ( ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) ↔ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) ) )
26 25 rabbidva ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ 𝑉 ∣ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑤 ) ) ≠ ( 0g ‘ 𝑀 ) } = { 𝑤 ∈ 𝑉 ∣ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) } )
27 neirr ⊢ ¬ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 )
28 27 a1i ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ¬ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) )
29 28 ralrimivw ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ∀ 𝑤 ∈ 𝑉 ¬ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) )
30 rabeq0 ⊢ ( { 𝑤 ∈ 𝑉 ∣ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) } = ∅ ↔ ∀ 𝑤 ∈ 𝑉 ¬ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) )
31 29 30 sylibr ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → { 𝑤 ∈ 𝑉 ∣ ( 0g ‘ 𝑀 ) ≠ ( 0g ‘ 𝑀 ) } = ∅ )
32 8 26 31 3eqtrd ⊢ ( ( ( 𝑀 ∈ Ring ∧ 𝑉 ∈ 𝑋 ∧ 𝐶 = ( 0g ‘ 𝑀 ) ) ∧ 𝐴 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 𝐶 ( .r ‘ 𝑀 ) ( 𝐴 ‘ 𝑣 ) ) ) supp ( 0g ‘ 𝑀 ) ) = ∅ )