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 )