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 )