Description: A Dirichlet character is a function. (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 ) |
||
dchrf.b | |- B = ( Base ` Z ) |
||
dchrf.x | |- ( ph -> X e. D ) |
||
Assertion | dchrf | |- ( ph -> X : B --> CC ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dchrmhm.g | |- G = ( DChr ` N ) |
|
2 | dchrmhm.z | |- Z = ( Z/nZ ` N ) |
|
3 | dchrmhm.b | |- D = ( Base ` G ) |
|
4 | dchrf.b | |- B = ( Base ` Z ) |
|
5 | dchrf.x | |- ( ph -> X e. D ) |
|
6 | eqid | |- ( Unit ` Z ) = ( Unit ` Z ) |
|
7 | 1 3 | dchrrcl | |- ( X e. D -> N e. NN ) |
8 | 5 7 | syl | |- ( ph -> N e. NN ) |
9 | 1 2 4 6 8 3 | dchrelbas3 | |- ( ph -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) ) ) |
10 | 5 9 | mpbid | |- ( ph -> ( X : B --> CC /\ ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) ) |
11 | 10 | simpld | |- ( ph -> X : B --> CC ) |