Metamath Proof Explorer


Theorem dchrmul

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 )
dchrmul.x
|- ( ph -> X e. D )
dchrmul.y
|- ( ph -> Y e. D )
Assertion dchrmul
|- ( ph -> ( X .x. Y ) = ( X oF x. Y ) )

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 dchrmul.x
 |-  ( ph -> X e. D )
6 dchrmul.y
 |-  ( ph -> Y e. D )
7 1 3 dchrrcl
 |-  ( X e. D -> N e. NN )
8 5 7 syl
 |-  ( ph -> N e. NN )
9 1 2 3 4 8 dchrplusg
 |-  ( ph -> .x. = ( oF x. |` ( D X. D ) ) )
10 9 oveqd
 |-  ( ph -> ( X .x. Y ) = ( X ( oF x. |` ( D X. D ) ) Y ) )
11 5 6 ofmresval
 |-  ( ph -> ( X ( oF x. |` ( D X. D ) ) Y ) = ( X oF x. Y ) )
12 10 11 eqtrd
 |-  ( ph -> ( X .x. Y ) = ( X oF x. Y ) )