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 
|- C = ( chr ` R )
chrid.l 
|- L = ( ZRHom ` R )
chrid.z 
|- .0. = ( 0g ` R )
Assertion chrcong 
|- ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( C || ( M - N ) <-> ( L ` M ) = ( L ` N ) ) )

Proof

Step Hyp Ref Expression
1 chrcl.c 
 |-  C = ( chr ` R )
2 chrid.l 
 |-  L = ( ZRHom ` R )
3 chrid.z 
 |-  .0. = ( 0g ` R )
4 eqid 
 |-  ( od ` R ) = ( od ` R )
5 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
6 4 5 1 chrval 
 |-  ( ( od ` R ) ` ( 1r ` R ) ) = C
7 6 breq1i 
 |-  ( ( ( od ` R ) ` ( 1r ` R ) ) || ( M - N ) <-> C || ( M - N ) )
8 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
9 8 3ad2ant1 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> R e. Grp )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 10 5 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
12 11 3ad2ant1 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( 1r ` R ) e. ( Base ` R ) )
13 simp2 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
14 simp3 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
15 eqid 
 |-  ( .g ` R ) = ( .g ` R )
16 10 4 15 3 odcong 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. ( Base ` R ) /\ ( M e. ZZ /\ N e. ZZ ) ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) || ( M - N ) <-> ( M ( .g ` R ) ( 1r ` R ) ) = ( N ( .g ` R ) ( 1r ` R ) ) ) )
17 9 12 13 14 16 syl112anc 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) || ( M - N ) <-> ( M ( .g ` R ) ( 1r ` R ) ) = ( N ( .g ` R ) ( 1r ` R ) ) ) )
18 7 17 bitr3id 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( C || ( M - N ) <-> ( M ( .g ` R ) ( 1r ` R ) ) = ( N ( .g ` R ) ( 1r ` R ) ) ) )
19 2 15 5 zrhmulg 
 |-  ( ( R e. Ring /\ M e. ZZ ) -> ( L ` M ) = ( M ( .g ` R ) ( 1r ` R ) ) )
20 19 3adant3 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( L ` M ) = ( M ( .g ` R ) ( 1r ` R ) ) )
21 2 15 5 zrhmulg 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( N ( .g ` R ) ( 1r ` R ) ) )
22 21 3adant2 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( L ` N ) = ( N ( .g ` R ) ( 1r ` R ) ) )
23 20 22 eqeq12d 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( ( L ` M ) = ( L ` N ) <-> ( M ( .g ` R ) ( 1r ` R ) ) = ( N ( .g ` R ) ( 1r ` R ) ) ) )
24 18 23 bitr4d 
 |-  ( ( R e. Ring /\ M e. ZZ /\ N e. ZZ ) -> ( C || ( M - N ) <-> ( L ` M ) = ( L ` N ) ) )