Metamath Proof Explorer

Theorem dchrelbas4

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g 
|- G = ( DChr ` N )
dchrmhm.z 
|- Z = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrelbas4.l 
|- L = ( ZRHom ` Z )
Assertion dchrelbas4 
|- ( X e. D <-> ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 
 |-  G = ( DChr ` N )
2 dchrmhm.z 
 |-  Z = ( Z/nZ ` N )
3 dchrmhm.b 
 |-  D = ( Base ` G )
4 dchrelbas4.l 
 |-  L = ( ZRHom ` Z )
5 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
6 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
7 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
8 id 
 |-  ( N e. NN -> N e. NN )
9 1 2 6 7 8 3 dchrelbas2 
 |-  ( N e. NN -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. y e. ( Base ` Z ) ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) ) ) )
10 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
11 10 adantr 
 |-  ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> N e. NN0 )
12 2 6 4 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
13 fveq2 
 |-  ( ( L ` x ) = y -> ( X ` ( L ` x ) ) = ( X ` y ) )
14 13 neeq1d 
 |-  ( ( L ` x ) = y -> ( ( X ` ( L ` x ) ) =/= 0 <-> ( X ` y ) =/= 0 ) )
15 eleq1 
 |-  ( ( L ` x ) = y -> ( ( L ` x ) e. ( Unit ` Z ) <-> y e. ( Unit ` Z ) ) )
16 14 15 imbi12d 
 |-  ( ( L ` x ) = y -> ( ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) ) )
17 16 cbvfo 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> ( A. x e. ZZ ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> A. y e. ( Base ` Z ) ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) ) )
18 11 12 17 3syl 
 |-  ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( A. x e. ZZ ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> A. y e. ( Base ` Z ) ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) ) )
19 df-ne 
 |-  ( ( X ` ( L ` x ) ) =/= 0 <-> -. ( X ` ( L ` x ) ) = 0 )
20 19 a1i 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( X ` ( L ` x ) ) =/= 0 <-> -. ( X ` ( L ` x ) ) = 0 ) )
21 2 7 4 znunit 
 |-  ( ( N e. NN0 /\ x e. ZZ ) -> ( ( L ` x ) e. ( Unit ` Z ) <-> ( x gcd N ) = 1 ) )
22 11 21 sylan 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( L ` x ) e. ( Unit ` Z ) <-> ( x gcd N ) = 1 ) )
23 1red 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> 1 e. RR )
24 simpr 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> x e. ZZ )
25 simpll 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> N e. NN )
26 25 nnzd 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> N e. ZZ )
27 nnne0 
 |-  ( N e. NN -> N =/= 0 )
28 simpr 
 |-  ( ( x = 0 /\ N = 0 ) -> N = 0 )
29 28 necon3ai 
 |-  ( N =/= 0 -> -. ( x = 0 /\ N = 0 ) )
30 25 27 29 3syl 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> -. ( x = 0 /\ N = 0 ) )
31 gcdn0cl 
 |-  ( ( ( x e. ZZ /\ N e. ZZ ) /\ -. ( x = 0 /\ N = 0 ) ) -> ( x gcd N ) e. NN )
32 24 26 30 31 syl21anc 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( x gcd N ) e. NN )
33 32 nnred 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( x gcd N ) e. RR )
34 32 nnge1d 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> 1 <_ ( x gcd N ) )
35 23 33 34 leltned 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( 1 < ( x gcd N ) <-> ( x gcd N ) =/= 1 ) )
36 35 necon2bbid 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( x gcd N ) = 1 <-> -. 1 < ( x gcd N ) ) )
37 22 36 bitrd 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( L ` x ) e. ( Unit ` Z ) <-> -. 1 < ( x gcd N ) ) )
38 20 37 imbi12d 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> ( -. ( X ` ( L ` x ) ) = 0 -> -. 1 < ( x gcd N ) ) ) )
39 con34b 
 |-  ( ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) <-> ( -. ( X ` ( L ` x ) ) = 0 -> -. 1 < ( x gcd N ) ) )
40 38 39 bitr4di 
 |-  ( ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ x e. ZZ ) -> ( ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )
41 40 ralbidva 
 |-  ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( A. x e. ZZ ( ( X ` ( L ` x ) ) =/= 0 -> ( L ` x ) e. ( Unit ` Z ) ) <-> A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )
42 18 41 bitr3d 
 |-  ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( A. y e. ( Base ` Z ) ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) <-> A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )
43 42 pm5.32da 
 |-  ( N e. NN -> ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. y e. ( Base ` Z ) ( ( X ` y ) =/= 0 -> y e. ( Unit ` Z ) ) ) <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) ) )
44 9 43 bitrd 
 |-  ( N e. NN -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) ) )
45 5 44 biadanii 
 |-  ( X e. D <-> ( N e. NN /\ ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) ) )
46 3anass 
 |-  ( ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) <-> ( N e. NN /\ ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) ) )
47 45 46 bitr4i 
 |-  ( X e. D <-> ( N e. NN /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. ZZ ( 1 < ( x gcd N ) -> ( X ` ( L ` x ) ) = 0 ) ) )