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	$⊢ C = chr (R)$
	chrid.l	$⊢ L = ℤRHom (R)$
	chrid.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	chrdvds	$⊢ (R \in Ring \land N \in ℤ) \to (C ∥ N \leftrightarrow L (N) = \underset{˙}{0})$

Step	Hyp	Ref	Expression
1		chrcl.c	$⊢ C = chr (R)$
2		chrid.l	$⊢ L = ℤRHom (R)$
3		chrid.z	$⊢ \underset{˙}{0} = 0_{R}$
4		eqid	$⊢ od (R) = od (R)$
5		eqid	$⊢ 1_{R} = 1_{R}$
6	4 5 1	chrval	$⊢ od (R) (1_{R}) = C$
7	6	breq1i	$⊢ od (R) (1_{R}) ∥ N \leftrightarrow C ∥ N$
8		ringgrp	$⊢ R \in Ring \to R \in Grp$
9	8	adantr	$⊢ (R \in Ring \land N \in ℤ) \to R \in Grp$
10		eqid	$⊢ {Base}_{R} = {Base}_{R}$
11	10 5	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
12	11	adantr	$⊢ (R \in Ring \land N \in ℤ) \to 1_{R} \in {Base}_{R}$
13		simpr	$⊢ (R \in Ring \land N \in ℤ) \to N \in ℤ$
14		eqid	$⊢ \cdot_{R} = \cdot_{R}$
15	10 4 14 3	oddvds	$⊢ (R \in Grp \land 1_{R} \in {Base}_{R} \land N \in ℤ) \to (od (R) (1_{R}) ∥ N \leftrightarrow N \cdot_{R} 1_{R} = \underset{˙}{0})$
16	9 12 13 15	syl3anc	$⊢ (R \in Ring \land N \in ℤ) \to (od (R) (1_{R}) ∥ N \leftrightarrow N \cdot_{R} 1_{R} = \underset{˙}{0})$
17	7 16	bitr3id	$⊢ (R \in Ring \land N \in ℤ) \to (C ∥ N \leftrightarrow N \cdot_{R} 1_{R} = \underset{˙}{0})$
18	2 14 5	zrhmulg	$⊢ (R \in Ring \land N \in ℤ) \to L (N) = N \cdot_{R} 1_{R}$
19	18	eqeq1d	$⊢ (R \in Ring \land N \in ℤ) \to (L (N) = \underset{˙}{0} \leftrightarrow N \cdot_{R} 1_{R} = \underset{˙}{0})$
20	17 19	bitr4d	$⊢ (R \in Ring \land N \in ℤ) \to (C ∥ N \leftrightarrow L (N) = \underset{˙}{0})$

Metamath Proof Explorer