Metamath Proof Explorer

Theorem dchrpt

Description: For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrpt.g 
|- G = ( DChr ` N )
dchrpt.z 
|- Z = ( Z/nZ ` N )
dchrpt.d 
|- D = ( Base ` G )
dchrpt.b 
|- B = ( Base ` Z )
dchrpt.1 
|- .1. = ( 1r ` Z )
dchrpt.n 
|- ( ph -> N e. NN )
dchrpt.n1 
|- ( ph -> A =/= .1. )
dchrpt.a 
|- ( ph -> A e. B )
Assertion dchrpt 
|- ( ph -> E. x e. D ( x ` A ) =/= 1 )

Proof

Step Hyp Ref Expression
1 dchrpt.g 
 |-  G = ( DChr ` N )
2 dchrpt.z 
 |-  Z = ( Z/nZ ` N )
3 dchrpt.d 
 |-  D = ( Base ` G )
4 dchrpt.b 
 |-  B = ( Base ` Z )
5 dchrpt.1 
 |-  .1. = ( 1r ` Z )
6 dchrpt.n 
 |-  ( ph -> N e. NN )
7 dchrpt.n1 
 |-  ( ph -> A =/= .1. )
8 dchrpt.a 
 |-  ( ph -> A e. B )
9 6 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> N e. NN )
10 7 ad3antrrr 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> A =/= .1. )
11 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
12 eqid 
 |-  ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) = ( ( mulGrp ` Z ) |`s ( Unit ` Z ) )
13 eqid 
 |-  ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) = ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) )
14 oveq1 
 |-  ( n = b -> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) = ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) )
15 14 cbvmptv 
 |-  ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) = ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) )
16 fveq2 
 |-  ( k = a -> ( w ` k ) = ( w ` a ) )
17 16 oveq2d 
 |-  ( k = a -> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) = ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` a ) ) )
18 17 mpteq2dv 
 |-  ( k = a -> ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) = ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` a ) ) ) )
19 15 18 syl5eq 
 |-  ( k = a -> ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) = ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` a ) ) ) )
20 19 rneqd 
 |-  ( k = a -> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) = ran ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` a ) ) ) )
21 20 cbvmptv 
 |-  ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) = ( a e. dom w |-> ran ( b e. ZZ |-> ( b ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` a ) ) ) )
22 simpllr 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> A e. ( Unit ` Z ) )
23 simplr 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> w e. Word ( Unit ` Z ) )
24 simprl 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) )
25 simprr 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) )
26 1 2 3 4 5 9 10 11 12 13 21 22 23 24 25 dchrptlem3 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> E. x e. D ( x ` A ) =/= 1 )
27 26 3adantr1 
 |-  ( ( ( ( ph /\ A e. ( Unit ` Z ) ) /\ w e. Word ( Unit ` Z ) ) /\ ( ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) : dom w --> { u e. ( SubGrp ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) | ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) |`s u ) e. ( CycGrp i^i ran pGrp ) } /\ ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) ) -> E. x e. D ( x ` A ) =/= 1 )
28 11 12 unitgrpbas 
 |-  ( Unit ` Z ) = ( Base ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) )
29 eqid 
 |-  { u e. ( SubGrp ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) | ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) |`s u ) e. ( CycGrp i^i ran pGrp ) } = { u e. ( SubGrp ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) | ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) |`s u ) e. ( CycGrp i^i ran pGrp ) }
30 6 nnnn0d 
 |-  ( ph -> N e. NN0 )
31 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
32 11 12 unitabl 
 |-  ( Z e. CRing -> ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) e. Abel )
33 30 31 32 3syl 
 |-  ( ph -> ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) e. Abel )
34 33 adantr 
 |-  ( ( ph /\ A e. ( Unit ` Z ) ) -> ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) e. Abel )
35 2 4 znfi 
 |-  ( N e. NN -> B e. Fin )
36 6 35 syl 
 |-  ( ph -> B e. Fin )
37 4 11 unitss 
 |-  ( Unit ` Z ) C_ B
38 ssfi 
 |-  ( ( B e. Fin /\ ( Unit ` Z ) C_ B ) -> ( Unit ` Z ) e. Fin )
39 36 37 38 sylancl 
 |-  ( ph -> ( Unit ` Z ) e. Fin )
40 39 adantr 
 |-  ( ( ph /\ A e. ( Unit ` Z ) ) -> ( Unit ` Z ) e. Fin )
41 eqid 
 |-  ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) = ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) )
42 28 29 34 40 13 41 ablfac2 
 |-  ( ( ph /\ A e. ( Unit ` Z ) ) -> E. w e. Word ( Unit ` Z ) ( ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) : dom w --> { u e. ( SubGrp ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) | ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) |`s u ) e. ( CycGrp i^i ran pGrp ) } /\ ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) dom DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) /\ ( ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) DProd ( k e. dom w |-> ran ( n e. ZZ |-> ( n ( .g ` ( ( mulGrp ` Z ) |`s ( Unit ` Z ) ) ) ( w ` k ) ) ) ) ) = ( Unit ` Z ) ) )
43 27 42 r19.29a 
 |-  ( ( ph /\ A e. ( Unit ` Z ) ) -> E. x e. D ( x ` A ) =/= 1 )
44 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
45 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
46 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
47 3 46 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. D )
48 6 44 45 47 4syl 
 |-  ( ph -> ( 0g ` G ) e. D )
49 0ne1 
 |-  0 =/= 1
50 1 2 3 4 11 48 8 dchrn0 
 |-  ( ph -> ( ( ( 0g ` G ) ` A ) =/= 0 <-> A e. ( Unit ` Z ) ) )
51 50 necon1bbid 
 |-  ( ph -> ( -. A e. ( Unit ` Z ) <-> ( ( 0g ` G ) ` A ) = 0 ) )
52 51 biimpa 
 |-  ( ( ph /\ -. A e. ( Unit ` Z ) ) -> ( ( 0g ` G ) ` A ) = 0 )
53 52 neeq1d 
 |-  ( ( ph /\ -. A e. ( Unit ` Z ) ) -> ( ( ( 0g ` G ) ` A ) =/= 1 <-> 0 =/= 1 ) )
54 49 53 mpbiri 
 |-  ( ( ph /\ -. A e. ( Unit ` Z ) ) -> ( ( 0g ` G ) ` A ) =/= 1 )
55 fveq1 
 |-  ( x = ( 0g ` G ) -> ( x ` A ) = ( ( 0g ` G ) ` A ) )
56 55 neeq1d 
 |-  ( x = ( 0g ` G ) -> ( ( x ` A ) =/= 1 <-> ( ( 0g ` G ) ` A ) =/= 1 ) )
57 56 rspcev 
 |-  ( ( ( 0g ` G ) e. D /\ ( ( 0g ` G ) ` A ) =/= 1 ) -> E. x e. D ( x ` A ) =/= 1 )
58 48 54 57 syl2an2r 
 |-  ( ( ph /\ -. A e. ( Unit ` Z ) ) -> E. x e. D ( x ` A ) =/= 1 )
59 43 58 pm2.61dan 
 |-  ( ph -> E. x e. D ( x ` A ) =/= 1 )