Metamath Proof Explorer

Theorem dchrval

Description: Value of the group of Dirichlet characters. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g 
|- G = ( DChr ` N )
dchrval.z 
|- Z = ( Z/nZ ` N )
dchrval.b 
|- B = ( Base ` Z )
dchrval.u 
|- U = ( Unit ` Z )
dchrval.n 
|- ( ph -> N e. NN )
dchrval.d 
|- ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
Assertion dchrval 
|- ( ph -> G = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )

Proof

Step Hyp Ref Expression
1 dchrval.g 
 |-  G = ( DChr ` N )
2 dchrval.z 
 |-  Z = ( Z/nZ ` N )
3 dchrval.b 
 |-  B = ( Base ` Z )
4 dchrval.u 
 |-  U = ( Unit ` Z )
5 dchrval.n 
 |-  ( ph -> N e. NN )
6 dchrval.d 
 |-  ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
7 df-dchr 
 |-  DChr = ( n e. NN |-> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } )
8 fvexd 
 |-  ( ( ph /\ n = N ) -> ( Z/nZ ` n ) e. _V )
9 ovex 
 |-  ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) e. _V
10 9 rabex 
 |-  { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } e. _V
11 10 a1i 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } e. _V )
12 6 ad2antrr 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
13 simpr 
 |-  ( ( ph /\ n = N ) -> n = N )
14 13 fveq2d 
 |-  ( ( ph /\ n = N ) -> ( Z/nZ ` n ) = ( Z/nZ ` N ) )
15 2 14 eqtr4id 
 |-  ( ( ph /\ n = N ) -> Z = ( Z/nZ ` n ) )
16 15 eqeq2d 
 |-  ( ( ph /\ n = N ) -> ( z = Z <-> z = ( Z/nZ ` n ) ) )
17 16 biimpar 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> z = Z )
18 17 fveq2d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( mulGrp ` z ) = ( mulGrp ` Z ) )
19 18 oveq1d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) = ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
20 17 fveq2d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( Base ` z ) = ( Base ` Z ) )
21 20 3 eqtr4di 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( Base ` z ) = B )
22 17 fveq2d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( Unit ` z ) = ( Unit ` Z ) )
23 22 4 eqtr4di 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( Unit ` z ) = U )
24 21 23 difeq12d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( ( Base ` z ) \ ( Unit ` z ) ) = ( B \ U ) )
25 24 xpeq1d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) = ( ( B \ U ) X. { 0 } ) )
26 25 sseq1d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x <-> ( ( B \ U ) X. { 0 } ) C_ x ) )
27 19 26 rabeqbidv 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( B \ U ) X. { 0 } ) C_ x } )
28 12 27 eqtr4d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> D = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } )
29 28 eqeq2d 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> ( b = D <-> b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) )
30 29 biimpar 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> b = D )
31 30 opeq2d 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , D >. )
32 30 sqxpeqd 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> ( b X. b ) = ( D X. D ) )
33 32 reseq2d 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> ( oF x. |` ( b X. b ) ) = ( oF x. |` ( D X. D ) ) )
34 33 opeq2d 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. = <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. )
35 31 34 preq12d 
 |-  ( ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) /\ b = { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } ) -> { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
36 11 35 csbied 
 |-  ( ( ( ph /\ n = N ) /\ z = ( Z/nZ ` n ) ) -> [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
37 8 36 csbied 
 |-  ( ( ph /\ n = N ) -> [_ ( Z/nZ ` n ) / z ]_ [_ { x e. ( ( mulGrp ` z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` z ) \ ( Unit ` z ) ) X. { 0 } ) C_ x } / b ]_ { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( oF x. |` ( b X. b ) ) >. } = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
38 prex 
 |-  { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } e. _V
39 38 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } e. _V )
40 7 37 5 39 fvmptd2 
 |-  ( ph -> ( DChr ` N ) = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
41 1 40 syl5eq 
 |-  ( ph -> G = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )