Metamath Proof Explorer

Theorem dchrabl

Description: The set of Dirichlet characters is an Abelian group. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypothesis dchrabl.g 
|- G = ( DChr ` N )
Assertion dchrabl 
|- ( N e. NN -> G e. Abel )

Proof

Step Hyp Ref Expression
1 dchrabl.g 
 |-  G = ( DChr ` N )
2 eqidd 
 |-  ( N e. NN -> ( Base ` G ) = ( Base ` G ) )
3 eqidd 
 |-  ( N e. NN -> ( +g ` G ) = ( +g ` G ) )
4 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
5 eqid 
 |-  ( Base ` G ) = ( Base ` G )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 simp2 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> x e. ( Base ` G ) )
8 simp3 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> y e. ( Base ` G ) )
9 1 4 5 6 7 8 dchrmulcl 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
10 fvexd 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( Base ` ( Z/nZ ` N ) ) e. _V )
11 eqid 
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
12 1 4 5 11 7 dchrf 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> x : ( Base ` ( Z/nZ ` N ) ) --> CC )
13 12 3adant3r3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x : ( Base ` ( Z/nZ ` N ) ) --> CC )
14 1 4 5 11 8 dchrf 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> y : ( Base ` ( Z/nZ ` N ) ) --> CC )
15 14 3adant3r3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> y : ( Base ` ( Z/nZ ` N ) ) --> CC )
16 simpr3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z e. ( Base ` G ) )
17 1 4 5 11 16 dchrf 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> z : ( Base ` ( Z/nZ ` N ) ) --> CC )
18 mulass 
 |-  ( ( a e. CC /\ b e. CC /\ c e. CC ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) )
19 18 adantl 
 |-  ( ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) /\ ( a e. CC /\ b e. CC /\ c e. CC ) ) -> ( ( a x. b ) x. c ) = ( a x. ( b x. c ) ) )
20 10 13 15 17 19 caofass 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x oF x. y ) oF x. z ) = ( x oF x. ( y oF x. z ) ) )
21 simpr1 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> x e. ( Base ` G ) )
22 simpr2 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> y e. ( Base ` G ) )
23 1 4 5 6 21 22 dchrmul 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) = ( x oF x. y ) )
24 23 oveq1d 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) oF x. z ) = ( ( x oF x. y ) oF x. z ) )
25 1 4 5 6 22 16 dchrmul 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) = ( y oF x. z ) )
26 25 oveq2d 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x oF x. ( y ( +g ` G ) z ) ) = ( x oF x. ( y oF x. z ) ) )
27 20 24 26 3eqtr4d 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) oF x. z ) = ( x oF x. ( y ( +g ` G ) z ) ) )
28 9 3adant3r3 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) y ) e. ( Base ` G ) )
29 1 4 5 6 28 16 dchrmul 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( ( x ( +g ` G ) y ) oF x. z ) )
30 1 4 5 6 22 16 dchrmulcl 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( y ( +g ` G ) z ) e. ( Base ` G ) )
31 1 4 5 6 21 30 dchrmul 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( x ( +g ` G ) ( y ( +g ` G ) z ) ) = ( x oF x. ( y ( +g ` G ) z ) ) )
32 27 29 31 3eqtr4d 
 |-  ( ( N e. NN /\ ( x e. ( Base ` G ) /\ y e. ( Base ` G ) /\ z e. ( Base ` G ) ) ) -> ( ( x ( +g ` G ) y ) ( +g ` G ) z ) = ( x ( +g ` G ) ( y ( +g ` G ) z ) ) )
33 eqid 
 |-  ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) )
34 eqid 
 |-  ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) )
35 id 
 |-  ( N e. NN -> N e. NN )
36 1 4 5 11 33 34 35 dchr1cl 
 |-  ( N e. NN -> ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) e. ( Base ` G ) )
37 simpr 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) ) -> x e. ( Base ` G ) )
38 1 4 5 11 33 34 6 37 dchrmulid2 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) ( +g ` G ) x ) = x )
39 eqid 
 |-  ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) )
40 1 4 5 11 33 34 6 37 39 dchrinvcl 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) e. ( Base ` G ) /\ ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) ( +g ` G ) x ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) ) )
41 40 simpld 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) e. ( Base ` G ) )
42 40 simprd 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) ) -> ( ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , ( 1 / ( x ` k ) ) , 0 ) ) ( +g ` G ) x ) = ( k e. ( Base ` ( Z/nZ ` N ) ) |-> if ( k e. ( Unit ` ( Z/nZ ` N ) ) , 1 , 0 ) ) )
43 2 3 9 32 36 38 41 42 isgrpd 
 |-  ( N e. NN -> G e. Grp )
44 fvexd 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( Base ` ( Z/nZ ` N ) ) e. _V )
45 mulcom 
 |-  ( ( a e. CC /\ b e. CC ) -> ( a x. b ) = ( b x. a ) )
46 45 adantl 
 |-  ( ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) /\ ( a e. CC /\ b e. CC ) ) -> ( a x. b ) = ( b x. a ) )
47 44 12 14 46 caofcom 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x oF x. y ) = ( y oF x. x ) )
48 1 4 5 6 7 8 dchrmul 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( x oF x. y ) )
49 1 4 5 6 8 7 dchrmul 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( y ( +g ` G ) x ) = ( y oF x. x ) )
50 47 48 49 3eqtr4d 
 |-  ( ( N e. NN /\ x e. ( Base ` G ) /\ y e. ( Base ` G ) ) -> ( x ( +g ` G ) y ) = ( y ( +g ` G ) x ) )
51 2 3 43 50 isabld 
 |-  ( N e. NN -> G e. Abel )