Metamath Proof Explorer

Theorem dchrplusg

Description: Group operation on the group of Dirichlet characters. (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 )
dchrmul.t 
|- .x. = ( +g ` G )
dchrplusg.n 
|- ( ph -> N e. NN )
Assertion dchrplusg 
|- ( ph -> .x. = ( oF x. |` ( D X. D ) ) )

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 dchrmul.t 
 |-  .x. = ( +g ` G )
5 dchrplusg.n 
 |-  ( ph -> N e. NN )
6 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
7 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
8 1 2 6 7 5 3 dchrbas 
 |-  ( ph -> D = { x e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) | ( ( ( Base ` Z ) \ ( Unit ` Z ) ) X. { 0 } ) C_ x } )
9 1 2 6 7 5 8 dchrval 
 |-  ( ph -> G = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
10 9 fveq2d 
 |-  ( ph -> ( +g ` G ) = ( +g ` { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } ) )
11 3 fvexi 
 |-  D e. _V
12 11 11 xpex 
 |-  ( D X. D ) e. _V
13 ofexg 
 |-  ( ( D X. D ) e. _V -> ( oF x. |` ( D X. D ) ) e. _V )
14 eqid 
 |-  { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } = { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. }
15 14 grpplusg 
 |-  ( ( oF x. |` ( D X. D ) ) e. _V -> ( oF x. |` ( D X. D ) ) = ( +g ` { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } ) )
16 12 13 15 mp2b 
 |-  ( oF x. |` ( D X. D ) ) = ( +g ` { <. ( Base ` ndx ) , D >. , <. ( +g ` ndx ) , ( oF x. |` ( D X. D ) ) >. } )
17 10 4 16 3eqtr4g 
 |-  ( ph -> .x. = ( oF x. |` ( D X. D ) ) )