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 ) ) |
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 ) ) |