This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdschrmulg

Description: In a ring, any multiple of the characteristics annihilates all elements. (Contributed by Thierry Arnoux, 6-Sep-2016)

Ref Expression
Hypotheses dvdschrmulg.1 ⊢ 𝐶 = ( chr ‘ 𝑅 )
dvdschrmulg.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
dvdschrmulg.3 ⊢ · = ( .g ‘ 𝑅 )
dvdschrmulg.4 ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion dvdschrmulg ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 · 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 dvdschrmulg.1 ⊢ 𝐶 = ( chr ‘ 𝑅 )
2 dvdschrmulg.2 ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 dvdschrmulg.3 ⊢ · = ( .g ‘ 𝑅 )
4 dvdschrmulg.4 ⊢ 0 = ( 0g ‘ 𝑅 )
5 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → 𝑅 ∈ Ring )
6 dvdszrcl ⊢ ( 𝐶 ∥ 𝑁 → ( 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
7 6 simprd ⊢ ( 𝐶 ∥ 𝑁 → 𝑁 ∈ ℤ )
8 7 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → 𝑁 ∈ ℤ )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 2 9 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
11 5 10 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
12 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
13 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
14 2 3 13 mulgass2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ∈ ℤ ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ 𝐴 ∈ 𝐵 ) ) → ( ( 𝑁 · ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 𝑁 · ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝐴 ) ) )
15 5 8 11 12 14 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑁 · ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 𝑁 · ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝐴 ) ) )
16 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
17 5 16 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → 𝑅 ∈ Grp )
18 eqid ⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
19 18 9 1 chrval ⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 𝐶
20 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → 𝐶 ∥ 𝑁 )
21 19 20 eqbrtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 )
22 2 18 3 4 oddvdsi ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ∧ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ) → ( 𝑁 · ( 1r ‘ 𝑅 ) ) = 0 )
23 17 11 21 22 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 · ( 1r ‘ 𝑅 ) ) = 0 )
24 23 oveq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑁 · ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝐴 ) = ( 0 ( .r ‘ 𝑅 ) 𝐴 ) )
25 2 13 4 ringlz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝐴 ) = 0 )
26 25 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 0 ( .r ‘ 𝑅 ) 𝐴 ) = 0 )
27 24 26 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑁 · ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝐴 ) = 0 )
28 2 13 9 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝐴 ) = 𝐴 )
29 28 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝐴 ) = 𝐴 )
30 29 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 · ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝐴 ) ) = ( 𝑁 · 𝐴 ) )
31 15 27 30 3eqtr3rd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∥ 𝑁 ∧ 𝐴 ∈ 𝐵 ) → ( 𝑁 · 𝐴 ) = 0 )