Theorem chrdvds

Description: The ZZ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	chrcl.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
	chrid.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	chrid.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	chrdvds	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝐿 ‘ 𝑁 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
2		chrid.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		chrid.z	⊢ 0 = ( 0g ‘ 𝑅 )
4		eqid	⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
5		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6	4 5 1	chrval	⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 𝐶
7	6	breq1i	⊢ ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ 𝐶 ∥ 𝑁 )
8		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
9	8	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → 𝑅 ∈ Grp )
10		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11	10 5	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12	11	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13		simpr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
14		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
15	10 4 14 3	oddvds	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
16	9 12 13 15	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
17	7 16	bitr3id	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
18	2 14 5	zrhmulg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
19	18	eqeq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑁 ) = 0 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
20	17 19	bitr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝐿 ‘ 𝑁 ) = 0 ) )