Theorem dchrresb

Description: A Dirichlet character is determined by its values on the unit group. (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	dchrresb.g	|- G = ( DChr ` N )
	dchrresb.z	|- Z = ( Z/nZ ` N )
	dchrresb.b	|- D = ( Base ` G )
	dchrresb.u	|- U = ( Unit ` Z )
	dchrresb.x	|- ( ph -> X e. D )
	dchrresb.Y	|- ( ph -> Y e. D )
Assertion	dchrresb	|- ( ph -> ( ( X |` U ) = ( Y |` U ) <-> X = Y ) )

Proof

Step	Hyp	Ref	Expression
1		dchrresb.g	|- G = ( DChr ` N )
2		dchrresb.z	|- Z = ( Z/nZ ` N )
3		dchrresb.b	|- D = ( Base ` G )
4		dchrresb.u	|- U = ( Unit ` Z )
5		dchrresb.x	|- ( ph -> X e. D )
6		dchrresb.Y	|- ( ph -> Y e. D )
7		eqid	|- ( Base ` Z ) = ( Base ` Z )
8	1 2 3 7 5	dchrf	|- ( ph -> X : ( Base ` Z ) --> CC )
9	8	ffnd	|- ( ph -> X Fn ( Base ` Z ) )
10	1 2 3 7 6	dchrf	|- ( ph -> Y : ( Base ` Z ) --> CC )
11	10	ffnd	|- ( ph -> Y Fn ( Base ` Z ) )
12	7 4	unitss	|- U C_ ( Base ` Z )
13		fvreseq	|- ( ( ( X Fn ( Base ` Z ) /\ Y Fn ( Base ` Z ) ) /\ U C_ ( Base ` Z ) ) -> ( ( X |` U ) = ( Y |` U ) <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
14	12 13	mpan2	|- ( ( X Fn ( Base ` Z ) /\ Y Fn ( Base ` Z ) ) -> ( ( X |` U ) = ( Y |` U ) <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
15	9 11 14	syl2anc	|- ( ph -> ( ( X |` U ) = ( Y |` U ) <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
16	1 2 3 4 5 6	dchreq	|- ( ph -> ( X = Y <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )
17	15 16	bitr4d	|- ( ph -> ( ( X |` U ) = ( Y |` U ) <-> X = Y ) )