This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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