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

Metamath Proof Explorer

Theorem dchrn0

Description: A Dirichlet character is nonzero on the 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 )
dchrn0.b 
|- B = ( Base ` Z )
dchrn0.u 
|- U = ( Unit ` Z )
dchrn0.x 
|- ( ph -> X e. D )
dchrn0.a 
|- ( ph -> A e. B )
Assertion dchrn0 
|- ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) )

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 dchrn0.b 
 |-  B = ( Base ` Z )
5 dchrn0.u 
 |-  U = ( Unit ` Z )
6 dchrn0.x 
 |-  ( ph -> X e. D )
7 dchrn0.a 
 |-  ( ph -> A e. B )
8 fveq2 
 |-  ( x = A -> ( X ` x ) = ( X ` A ) )
9 8 neeq1d 
 |-  ( x = A -> ( ( X ` x ) =/= 0 <-> ( X ` A ) =/= 0 ) )
10 eleq1 
 |-  ( x = A -> ( x e. U <-> A e. U ) )
11 9 10 imbi12d 
 |-  ( x = A -> ( ( ( X ` x ) =/= 0 -> x e. U ) <-> ( ( X ` A ) =/= 0 -> A e. U ) ) )
12 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
13 6 12 syl 
 |-  ( ph -> N e. NN )
14 1 2 4 5 13 3 dchrelbas2 
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )
15 6 14 mpbid 
 |-  ( ph -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) )
16 15 simprd 
 |-  ( ph -> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) )
17 11 16 7 rspcdva 
 |-  ( ph -> ( ( X ` A ) =/= 0 -> A e. U ) )
18 17 imp 
 |-  ( ( ph /\ ( X ` A ) =/= 0 ) -> A e. U )
19 ax-1ne0 
 |-  1 =/= 0
20 19 a1i 
 |-  ( ( ph /\ A e. U ) -> 1 =/= 0 )
21 13 nnnn0d 
 |-  ( ph -> N e. NN0 )
22 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
23 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
24 21 22 23 3syl 
 |-  ( ph -> Z e. Ring )
25 eqid 
 |-  ( invr ` Z ) = ( invr ` Z )
26 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
27 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
28 5 25 26 27 unitrinv 
 |-  ( ( Z e. Ring /\ A e. U ) -> ( A ( .r ` Z ) ( ( invr ` Z ) ` A ) ) = ( 1r ` Z ) )
29 24 28 sylan 
 |-  ( ( ph /\ A e. U ) -> ( A ( .r ` Z ) ( ( invr ` Z ) ` A ) ) = ( 1r ` Z ) )
30 29 fveq2d 
 |-  ( ( ph /\ A e. U ) -> ( X ` ( A ( .r ` Z ) ( ( invr ` Z ) ` A ) ) ) = ( X ` ( 1r ` Z ) ) )
31 15 simpld 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
32 31 adantr 
 |-  ( ( ph /\ A e. U ) -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
33 7 adantr 
 |-  ( ( ph /\ A e. U ) -> A e. B )
34 5 25 4 ringinvcl 
 |-  ( ( Z e. Ring /\ A e. U ) -> ( ( invr ` Z ) ` A ) e. B )
35 24 34 sylan 
 |-  ( ( ph /\ A e. U ) -> ( ( invr ` Z ) ` A ) e. B )
36 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
37 36 4 mgpbas 
 |-  B = ( Base ` ( mulGrp ` Z ) )
38 36 26 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
39 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
40 cnfldmul 
 |-  x. = ( .r ` CCfld )
41 39 40 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
42 37 38 41 mhmlin 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A e. B /\ ( ( invr ` Z ) ` A ) e. B ) -> ( X ` ( A ( .r ` Z ) ( ( invr ` Z ) ` A ) ) ) = ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) )
43 32 33 35 42 syl3anc 
 |-  ( ( ph /\ A e. U ) -> ( X ` ( A ( .r ` Z ) ( ( invr ` Z ) ` A ) ) ) = ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) )
44 36 27 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
45 cnfld1 
 |-  1 = ( 1r ` CCfld )
46 39 45 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
47 44 46 mhm0 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 )
48 32 47 syl 
 |-  ( ( ph /\ A e. U ) -> ( X ` ( 1r ` Z ) ) = 1 )
49 30 43 48 3eqtr3d 
 |-  ( ( ph /\ A e. U ) -> ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) = 1 )
50 cnfldbas 
 |-  CC = ( Base ` CCfld )
51 39 50 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
52 37 51 mhmf 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> X : B --> CC )
53 32 52 syl 
 |-  ( ( ph /\ A e. U ) -> X : B --> CC )
54 53 35 ffvelcdmd 
 |-  ( ( ph /\ A e. U ) -> ( X ` ( ( invr ` Z ) ` A ) ) e. CC )
55 54 mul02d 
 |-  ( ( ph /\ A e. U ) -> ( 0 x. ( X ` ( ( invr ` Z ) ` A ) ) ) = 0 )
56 20 49 55 3netr4d 
 |-  ( ( ph /\ A e. U ) -> ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) =/= ( 0 x. ( X ` ( ( invr ` Z ) ` A ) ) ) )
57 oveq1 
 |-  ( ( X ` A ) = 0 -> ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) = ( 0 x. ( X ` ( ( invr ` Z ) ` A ) ) ) )
58 57 necon3i 
 |-  ( ( ( X ` A ) x. ( X ` ( ( invr ` Z ) ` A ) ) ) =/= ( 0 x. ( X ` ( ( invr ` Z ) ` A ) ) ) -> ( X ` A ) =/= 0 )
59 56 58 syl 
 |-  ( ( ph /\ A e. U ) -> ( X ` A ) =/= 0 )
60 18 59 impbida 
 |-  ( ph -> ( ( X ` A ) =/= 0 <-> A e. U ) )