Metamath Proof Explorer

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

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 ) ) || N <-> C || N )
8 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
9 8 adantr 
 |-  ( ( R e. Ring /\ 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 adantr 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( 1r ` R ) e. ( Base ` R ) )
13 simpr 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> N e. ZZ )
14 eqid 
 |-  ( .g ` R ) = ( .g ` R )
15 10 4 14 3 oddvds 
 |-  ( ( R e. Grp /\ ( 1r ` R ) e. ( Base ` R ) /\ N e. ZZ ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) || N <-> ( N ( .g ` R ) ( 1r ` R ) ) = .0. ) )
16 9 12 13 15 syl3anc 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) || N <-> ( N ( .g ` R ) ( 1r ` R ) ) = .0. ) )
17 7 16 bitr3id 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( C || N <-> ( N ( .g ` R ) ( 1r ` R ) ) = .0. ) )
18 2 14 5 zrhmulg 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( L ` N ) = ( N ( .g ` R ) ( 1r ` R ) ) )
19 18 eqeq1d 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( ( L ` N ) = .0. <-> ( N ( .g ` R ) ( 1r ` R ) ) = .0. ) )
20 17 19 bitr4d 
 |-  ( ( R e. Ring /\ N e. ZZ ) -> ( C || N <-> ( L ` N ) = .0. ) )