chrcong

Description: If two integers are congruent relative to the ring characteristic, their images in the ring are the same. (Contributed by Mario Carneiro, 24-Sep-2015)

	Ref	Expression
Hypotheses	chrcl.c	$⊢ C = chr (R)$
	chrid.l	$⊢ L = ℤRHom (R)$
	chrid.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	chrcong	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to (C ∥ (M - N) \leftrightarrow L (M) = L (N))$

Proof

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}) ∥ (M - N) \leftrightarrow C ∥ (M - N)$
8		ringgrp	$⊢ R \in Ring \to R \in Grp$
9	8	3ad2ant1	$⊢ (R \in Ring \land M \in ℤ \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	3ad2ant1	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to 1_{R} \in {Base}_{R}$
13		simp2	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to M \in ℤ$
14		simp3	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to N \in ℤ$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	10 4 15 3	odcong	$⊢ (R \in Grp \land 1_{R} \in {Base}_{R} \land (M \in ℤ \land N \in ℤ)) \to (od (R) (1_{R}) ∥ (M - N) \leftrightarrow M \cdot_{R} 1_{R} = N \cdot_{R} 1_{R})$
17	9 12 13 14 16	syl112anc	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to (od (R) (1_{R}) ∥ (M - N) \leftrightarrow M \cdot_{R} 1_{R} = N \cdot_{R} 1_{R})$
18	7 17	bitr3id	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to (C ∥ (M - N) \leftrightarrow M \cdot_{R} 1_{R} = N \cdot_{R} 1_{R})$
19	2 15 5	zrhmulg	$⊢ (R \in Ring \land M \in ℤ) \to L (M) = M \cdot_{R} 1_{R}$
20	19	3adant3	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to L (M) = M \cdot_{R} 1_{R}$
21	2 15 5	zrhmulg	$⊢ (R \in Ring \land N \in ℤ) \to L (N) = N \cdot_{R} 1_{R}$
22	21	3adant2	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to L (N) = N \cdot_{R} 1_{R}$
23	20 22	eqeq12d	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to (L (M) = L (N) \leftrightarrow M \cdot_{R} 1_{R} = N \cdot_{R} 1_{R})$
24	18 23	bitr4d	$⊢ (R \in Ring \land M \in ℤ \land N \in ℤ) \to (C ∥ (M - N) \leftrightarrow L (M) = L (N))$

Metamath Proof Explorer

Theorem chrcong

Proof