Metamath Proof Explorer

Theorem dchreq

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 dchreq 
|- ( ph -> ( X = Y <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )

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 eldif 
 |-  ( k e. ( ( Base ` Z ) \ U ) <-> ( k e. ( Base ` Z ) /\ -. k e. U ) )
8 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
9 5 adantr 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> X e. D )
10 simpr 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> k e. ( Base ` Z ) )
11 1 2 3 8 4 9 10 dchrn0 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( ( X ` k ) =/= 0 <-> k e. U ) )
12 11 biimpd 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( ( X ` k ) =/= 0 -> k e. U ) )
13 12 necon1bd 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( -. k e. U -> ( X ` k ) = 0 ) )
14 13 impr 
 |-  ( ( ph /\ ( k e. ( Base ` Z ) /\ -. k e. U ) ) -> ( X ` k ) = 0 )
15 7 14 sylan2b 
 |-  ( ( ph /\ k e. ( ( Base ` Z ) \ U ) ) -> ( X ` k ) = 0 )
16 6 adantr 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> Y e. D )
17 1 2 3 8 4 16 10 dchrn0 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( ( Y ` k ) =/= 0 <-> k e. U ) )
18 17 biimpd 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( ( Y ` k ) =/= 0 -> k e. U ) )
19 18 necon1bd 
 |-  ( ( ph /\ k e. ( Base ` Z ) ) -> ( -. k e. U -> ( Y ` k ) = 0 ) )
20 19 impr 
 |-  ( ( ph /\ ( k e. ( Base ` Z ) /\ -. k e. U ) ) -> ( Y ` k ) = 0 )
21 7 20 sylan2b 
 |-  ( ( ph /\ k e. ( ( Base ` Z ) \ U ) ) -> ( Y ` k ) = 0 )
22 15 21 eqtr4d 
 |-  ( ( ph /\ k e. ( ( Base ` Z ) \ U ) ) -> ( X ` k ) = ( Y ` k ) )
23 22 ralrimiva 
 |-  ( ph -> A. k e. ( ( Base ` Z ) \ U ) ( X ` k ) = ( Y ` k ) )
24 1 2 3 8 5 dchrf 
 |-  ( ph -> X : ( Base ` Z ) --> CC )
25 24 ffnd 
 |-  ( ph -> X Fn ( Base ` Z ) )
26 1 2 3 8 6 dchrf 
 |-  ( ph -> Y : ( Base ` Z ) --> CC )
27 26 ffnd 
 |-  ( ph -> Y Fn ( Base ` Z ) )
28 eqfnfv 
 |-  ( ( X Fn ( Base ` Z ) /\ Y Fn ( Base ` Z ) ) -> ( X = Y <-> A. k e. ( Base ` Z ) ( X ` k ) = ( Y ` k ) ) )
29 25 27 28 syl2anc 
 |-  ( ph -> ( X = Y <-> A. k e. ( Base ` Z ) ( X ` k ) = ( Y ` k ) ) )
30 8 4 unitss 
 |-  U C_ ( Base ` Z )
31 undif 
 |-  ( U C_ ( Base ` Z ) <-> ( U u. ( ( Base ` Z ) \ U ) ) = ( Base ` Z ) )
32 30 31 mpbi 
 |-  ( U u. ( ( Base ` Z ) \ U ) ) = ( Base ` Z )
33 32 raleqi 
 |-  ( A. k e. ( U u. ( ( Base ` Z ) \ U ) ) ( X ` k ) = ( Y ` k ) <-> A. k e. ( Base ` Z ) ( X ` k ) = ( Y ` k ) )
34 ralunb 
 |-  ( A. k e. ( U u. ( ( Base ` Z ) \ U ) ) ( X ` k ) = ( Y ` k ) <-> ( A. k e. U ( X ` k ) = ( Y ` k ) /\ A. k e. ( ( Base ` Z ) \ U ) ( X ` k ) = ( Y ` k ) ) )
35 33 34 bitr3i 
 |-  ( A. k e. ( Base ` Z ) ( X ` k ) = ( Y ` k ) <-> ( A. k e. U ( X ` k ) = ( Y ` k ) /\ A. k e. ( ( Base ` Z ) \ U ) ( X ` k ) = ( Y ` k ) ) )
36 29 35 bitrdi 
 |-  ( ph -> ( X = Y <-> ( A. k e. U ( X ` k ) = ( Y ` k ) /\ A. k e. ( ( Base ` Z ) \ U ) ( X ` k ) = ( Y ` k ) ) ) )
37 23 36 mpbiran2d 
 |-  ( ph -> ( X = Y <-> A. k e. U ( X ` k ) = ( Y ` k ) ) )