This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ 𝐶 = ( chr ‘ 𝑅 )
chrid.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
chrid.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion chrcong ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝐿 ‘ 𝑀 ) = ( 𝐿 ‘ 𝑁 ) ) )

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 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑅 ∈ Grp )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 5 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 11 3ad2ant1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
14 simp3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
15 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
16 10 4 15 3 odcong ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
17 9 12 13 14 16 syl112anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
18 7 17 bitr3id ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
19 2 15 5 zrhmulg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ) → ( 𝐿 ‘ 𝑀 ) = ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
20 19 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑀 ) = ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
21 2 15 5 zrhmulg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
22 21 3adant2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
23 20 22 eqeq12d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑀 ) = ( 𝐿 ‘ 𝑁 ) ↔ ( 𝑀 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
24 18 23 bitr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ ( 𝑀 − 𝑁 ) ↔ ( 𝐿 ‘ 𝑀 ) = ( 𝐿 ‘ 𝑁 ) ) )