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 )