Metamath Proof Explorer


Theorem dchrf

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 )

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