Metamath Proof Explorer

Theorem dchrhash

Description: There are exactly phi ( N ) Dirichlet characters modulo N . Part of Theorem 6.5.1 of Shapiro p. 230. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses sumdchr.g 
|- G = ( DChr ` N )
sumdchr.d 
|- D = ( Base ` G )
Assertion dchrhash 
|- ( N e. NN -> ( # ` D ) = ( phi ` N ) )

Proof

Step Hyp Ref Expression
1 sumdchr.g 
 |-  G = ( DChr ` N )
2 sumdchr.d 
 |-  D = ( Base ` G )
3 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
4 eqid 
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
5 3 4 znfi 
 |-  ( N e. NN -> ( Base ` ( Z/nZ ` N ) ) e. Fin )
6 1 2 dchrfi 
 |-  ( N e. NN -> D e. Fin )
7 simprr 
 |-  ( ( N e. NN /\ ( a e. ( Base ` ( Z/nZ ` N ) ) /\ x e. D ) ) -> x e. D )
8 1 3 2 4 7 dchrf 
 |-  ( ( N e. NN /\ ( a e. ( Base ` ( Z/nZ ` N ) ) /\ x e. D ) ) -> x : ( Base ` ( Z/nZ ` N ) ) --> CC )
9 simprl 
 |-  ( ( N e. NN /\ ( a e. ( Base ` ( Z/nZ ` N ) ) /\ x e. D ) ) -> a e. ( Base ` ( Z/nZ ` N ) ) )
10 8 9 ffvelrnd 
 |-  ( ( N e. NN /\ ( a e. ( Base ` ( Z/nZ ` N ) ) /\ x e. D ) ) -> ( x ` a ) e. CC )
11 5 6 10 fsumcom 
 |-  ( N e. NN -> sum_ a e. ( Base ` ( Z/nZ ` N ) ) sum_ x e. D ( x ` a ) = sum_ x e. D sum_ a e. ( Base ` ( Z/nZ ` N ) ) ( x ` a ) )
12 eqid 
 |-  ( 1r ` ( Z/nZ ` N ) ) = ( 1r ` ( Z/nZ ` N ) )
13 simpl 
 |-  ( ( N e. NN /\ a e. ( Base ` ( Z/nZ ` N ) ) ) -> N e. NN )
14 simpr 
 |-  ( ( N e. NN /\ a e. ( Base ` ( Z/nZ ` N ) ) ) -> a e. ( Base ` ( Z/nZ ` N ) ) )
15 1 2 3 12 4 13 14 sumdchr2 
 |-  ( ( N e. NN /\ a e. ( Base ` ( Z/nZ ` N ) ) ) -> sum_ x e. D ( x ` a ) = if ( a = ( 1r ` ( Z/nZ ` N ) ) , ( # ` D ) , 0 ) )
16 velsn 
 |-  ( a e. { ( 1r ` ( Z/nZ ` N ) ) } <-> a = ( 1r ` ( Z/nZ ` N ) ) )
17 ifbi 
 |-  ( ( a e. { ( 1r ` ( Z/nZ ` N ) ) } <-> a = ( 1r ` ( Z/nZ ` N ) ) ) -> if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) = if ( a = ( 1r ` ( Z/nZ ` N ) ) , ( # ` D ) , 0 ) )
18 16 17 mp1i 
 |-  ( ( N e. NN /\ a e. ( Base ` ( Z/nZ ` N ) ) ) -> if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) = if ( a = ( 1r ` ( Z/nZ ` N ) ) , ( # ` D ) , 0 ) )
19 15 18 eqtr4d 
 |-  ( ( N e. NN /\ a e. ( Base ` ( Z/nZ ` N ) ) ) -> sum_ x e. D ( x ` a ) = if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) )
20 19 sumeq2dv 
 |-  ( N e. NN -> sum_ a e. ( Base ` ( Z/nZ ` N ) ) sum_ x e. D ( x ` a ) = sum_ a e. ( Base ` ( Z/nZ ` N ) ) if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) )
21 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
22 simpr 
 |-  ( ( N e. NN /\ x e. D ) -> x e. D )
23 1 3 2 21 22 4 dchrsum 
 |-  ( ( N e. NN /\ x e. D ) -> sum_ a e. ( Base ` ( Z/nZ ` N ) ) ( x ` a ) = if ( x = ( 0g ` G ) , ( phi ` N ) , 0 ) )
24 velsn 
 |-  ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) )
25 ifbi 
 |-  ( ( x e. { ( 0g ` G ) } <-> x = ( 0g ` G ) ) -> if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) = if ( x = ( 0g ` G ) , ( phi ` N ) , 0 ) )
26 24 25 mp1i 
 |-  ( ( N e. NN /\ x e. D ) -> if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) = if ( x = ( 0g ` G ) , ( phi ` N ) , 0 ) )
27 23 26 eqtr4d 
 |-  ( ( N e. NN /\ x e. D ) -> sum_ a e. ( Base ` ( Z/nZ ` N ) ) ( x ` a ) = if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) )
28 27 sumeq2dv 
 |-  ( N e. NN -> sum_ x e. D sum_ a e. ( Base ` ( Z/nZ ` N ) ) ( x ` a ) = sum_ x e. D if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) )
29 11 20 28 3eqtr3d 
 |-  ( N e. NN -> sum_ a e. ( Base ` ( Z/nZ ` N ) ) if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) = sum_ x e. D if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) )
30 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
31 3 zncrng 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
32 crngring 
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Z/nZ ` N ) e. Ring )
33 4 12 ringidcl 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
34 30 31 32 33 4syl 
 |-  ( N e. NN -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
35 34 snssd 
 |-  ( N e. NN -> { ( 1r ` ( Z/nZ ` N ) ) } C_ ( Base ` ( Z/nZ ` N ) ) )
36 hashcl 
 |-  ( D e. Fin -> ( # ` D ) e. NN0 )
37 nn0cn 
 |-  ( ( # ` D ) e. NN0 -> ( # ` D ) e. CC )
38 6 36 37 3syl 
 |-  ( N e. NN -> ( # ` D ) e. CC )
39 38 ralrimivw 
 |-  ( N e. NN -> A. a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) e. CC )
40 5 olcd 
 |-  ( N e. NN -> ( ( Base ` ( Z/nZ ` N ) ) C_ ( ZZ>= ` 0 ) \/ ( Base ` ( Z/nZ ` N ) ) e. Fin ) )
41 sumss2 
 |-  ( ( ( { ( 1r ` ( Z/nZ ` N ) ) } C_ ( Base ` ( Z/nZ ` N ) ) /\ A. a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) e. CC ) /\ ( ( Base ` ( Z/nZ ` N ) ) C_ ( ZZ>= ` 0 ) \/ ( Base ` ( Z/nZ ` N ) ) e. Fin ) ) -> sum_ a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) = sum_ a e. ( Base ` ( Z/nZ ` N ) ) if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) )
42 35 39 40 41 syl21anc 
 |-  ( N e. NN -> sum_ a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) = sum_ a e. ( Base ` ( Z/nZ ` N ) ) if ( a e. { ( 1r ` ( Z/nZ ` N ) ) } , ( # ` D ) , 0 ) )
43 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
44 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
45 2 21 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. D )
46 43 44 45 3syl 
 |-  ( N e. NN -> ( 0g ` G ) e. D )
47 46 snssd 
 |-  ( N e. NN -> { ( 0g ` G ) } C_ D )
48 phicl 
 |-  ( N e. NN -> ( phi ` N ) e. NN )
49 48 nncnd 
 |-  ( N e. NN -> ( phi ` N ) e. CC )
50 49 ralrimivw 
 |-  ( N e. NN -> A. x e. { ( 0g ` G ) } ( phi ` N ) e. CC )
51 6 olcd 
 |-  ( N e. NN -> ( D C_ ( ZZ>= ` 0 ) \/ D e. Fin ) )
52 sumss2 
 |-  ( ( ( { ( 0g ` G ) } C_ D /\ A. x e. { ( 0g ` G ) } ( phi ` N ) e. CC ) /\ ( D C_ ( ZZ>= ` 0 ) \/ D e. Fin ) ) -> sum_ x e. { ( 0g ` G ) } ( phi ` N ) = sum_ x e. D if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) )
53 47 50 51 52 syl21anc 
 |-  ( N e. NN -> sum_ x e. { ( 0g ` G ) } ( phi ` N ) = sum_ x e. D if ( x e. { ( 0g ` G ) } , ( phi ` N ) , 0 ) )
54 29 42 53 3eqtr4d 
 |-  ( N e. NN -> sum_ a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) = sum_ x e. { ( 0g ` G ) } ( phi ` N ) )
55 eqidd 
 |-  ( a = ( 1r ` ( Z/nZ ` N ) ) -> ( # ` D ) = ( # ` D ) )
56 55 sumsn 
 |-  ( ( ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) /\ ( # ` D ) e. CC ) -> sum_ a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) = ( # ` D ) )
57 34 38 56 syl2anc 
 |-  ( N e. NN -> sum_ a e. { ( 1r ` ( Z/nZ ` N ) ) } ( # ` D ) = ( # ` D ) )
58 eqidd 
 |-  ( x = ( 0g ` G ) -> ( phi ` N ) = ( phi ` N ) )
59 58 sumsn 
 |-  ( ( ( 0g ` G ) e. D /\ ( phi ` N ) e. CC ) -> sum_ x e. { ( 0g ` G ) } ( phi ` N ) = ( phi ` N ) )
60 46 49 59 syl2anc 
 |-  ( N e. NN -> sum_ x e. { ( 0g ` G ) } ( phi ` N ) = ( phi ` N ) )
61 54 57 60 3eqtr3d 
 |-  ( N e. NN -> ( # ` D ) = ( phi ` N ) )