Metamath Proof Explorer

Theorem dchrelbas2

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g 
|- G = ( DChr ` N )
dchrval.z 
|- Z = ( Z/nZ ` N )
dchrval.b 
|- B = ( Base ` Z )
dchrval.u 
|- U = ( Unit ` Z )
dchrval.n 
|- ( ph -> N e. NN )
dchrbas.b 
|- D = ( Base ` G )
Assertion dchrelbas2 
|- ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )

Proof

Step Hyp Ref Expression
1 dchrval.g 
 |-  G = ( DChr ` N )
2 dchrval.z 
 |-  Z = ( Z/nZ ` N )
3 dchrval.b 
 |-  B = ( Base ` Z )
4 dchrval.u 
 |-  U = ( Unit ` Z )
5 dchrval.n 
 |-  ( ph -> N e. NN )
6 dchrbas.b 
 |-  D = ( Base ` G )
7 1 2 3 4 5 6 dchrelbas 
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) ) )
8 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
9 8 3 mgpbas 
 |-  B = ( Base ` ( mulGrp ` Z ) )
10 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
11 cnfldbas 
 |-  CC = ( Base ` CCfld )
12 10 11 mgpbas 
 |-  CC = ( Base ` ( mulGrp ` CCfld ) )
13 9 12 mhmf 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> X : B --> CC )
14 13 adantl 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> X : B --> CC )
15 14 ffund 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> Fun X )
16 funssres 
 |-  ( ( Fun X /\ ( ( B \ U ) X. { 0 } ) C_ X ) -> ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) )
17 15 16 sylan 
 |-  ( ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) -> ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) )
18 simpr 
 |-  ( ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) ) -> ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) )
19 resss 
 |-  ( X |` dom ( ( B \ U ) X. { 0 } ) ) C_ X
20 18 19 eqsstrrdi 
 |-  ( ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) /\ ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) ) -> ( ( B \ U ) X. { 0 } ) C_ X )
21 17 20 impbida 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( ( B \ U ) X. { 0 } ) C_ X <-> ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) ) )
22 0cn 
 |-  0 e. CC
23 fconst6g 
 |-  ( 0 e. CC -> ( ( B \ U ) X. { 0 } ) : ( B \ U ) --> CC )
24 22 23 mp1i 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( B \ U ) X. { 0 } ) : ( B \ U ) --> CC )
25 24 fdmd 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> dom ( ( B \ U ) X. { 0 } ) = ( B \ U ) )
26 25 reseq2d 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( X |` ( B \ U ) ) )
27 26 eqeq1d 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( X |` dom ( ( B \ U ) X. { 0 } ) ) = ( ( B \ U ) X. { 0 } ) <-> ( X |` ( B \ U ) ) = ( ( B \ U ) X. { 0 } ) ) )
28 difss 
 |-  ( B \ U ) C_ B
29 fssres 
 |-  ( ( X : B --> CC /\ ( B \ U ) C_ B ) -> ( X |` ( B \ U ) ) : ( B \ U ) --> CC )
30 14 28 29 sylancl 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( X |` ( B \ U ) ) : ( B \ U ) --> CC )
31 30 ffnd 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( X |` ( B \ U ) ) Fn ( B \ U ) )
32 24 ffnd 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( B \ U ) X. { 0 } ) Fn ( B \ U ) )
33 eqfnfv 
 |-  ( ( ( X |` ( B \ U ) ) Fn ( B \ U ) /\ ( ( B \ U ) X. { 0 } ) Fn ( B \ U ) ) -> ( ( X |` ( B \ U ) ) = ( ( B \ U ) X. { 0 } ) <-> A. x e. ( B \ U ) ( ( X |` ( B \ U ) ) ` x ) = ( ( ( B \ U ) X. { 0 } ) ` x ) ) )
34 31 32 33 syl2anc 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( X |` ( B \ U ) ) = ( ( B \ U ) X. { 0 } ) <-> A. x e. ( B \ U ) ( ( X |` ( B \ U ) ) ` x ) = ( ( ( B \ U ) X. { 0 } ) ` x ) ) )
35 fvres 
 |-  ( x e. ( B \ U ) -> ( ( X |` ( B \ U ) ) ` x ) = ( X ` x ) )
36 c0ex 
 |-  0 e. _V
37 36 fvconst2 
 |-  ( x e. ( B \ U ) -> ( ( ( B \ U ) X. { 0 } ) ` x ) = 0 )
38 35 37 eqeq12d 
 |-  ( x e. ( B \ U ) -> ( ( ( X |` ( B \ U ) ) ` x ) = ( ( ( B \ U ) X. { 0 } ) ` x ) <-> ( X ` x ) = 0 ) )
39 38 ralbiia 
 |-  ( A. x e. ( B \ U ) ( ( X |` ( B \ U ) ) ` x ) = ( ( ( B \ U ) X. { 0 } ) ` x ) <-> A. x e. ( B \ U ) ( X ` x ) = 0 )
40 eldif 
 |-  ( x e. ( B \ U ) <-> ( x e. B /\ -. x e. U ) )
41 40 imbi1i 
 |-  ( ( x e. ( B \ U ) -> ( X ` x ) = 0 ) <-> ( ( x e. B /\ -. x e. U ) -> ( X ` x ) = 0 ) )
42 impexp 
 |-  ( ( ( x e. B /\ -. x e. U ) -> ( X ` x ) = 0 ) <-> ( x e. B -> ( -. x e. U -> ( X ` x ) = 0 ) ) )
43 con1b 
 |-  ( ( -. x e. U -> ( X ` x ) = 0 ) <-> ( -. ( X ` x ) = 0 -> x e. U ) )
44 df-ne 
 |-  ( ( X ` x ) =/= 0 <-> -. ( X ` x ) = 0 )
45 44 imbi1i 
 |-  ( ( ( X ` x ) =/= 0 -> x e. U ) <-> ( -. ( X ` x ) = 0 -> x e. U ) )
46 43 45 bitr4i 
 |-  ( ( -. x e. U -> ( X ` x ) = 0 ) <-> ( ( X ` x ) =/= 0 -> x e. U ) )
47 46 imbi2i 
 |-  ( ( x e. B -> ( -. x e. U -> ( X ` x ) = 0 ) ) <-> ( x e. B -> ( ( X ` x ) =/= 0 -> x e. U ) ) )
48 41 42 47 3bitri 
 |-  ( ( x e. ( B \ U ) -> ( X ` x ) = 0 ) <-> ( x e. B -> ( ( X ` x ) =/= 0 -> x e. U ) ) )
49 48 ralbii2 
 |-  ( A. x e. ( B \ U ) ( X ` x ) = 0 <-> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) )
50 39 49 bitri 
 |-  ( A. x e. ( B \ U ) ( ( X |` ( B \ U ) ) ` x ) = ( ( ( B \ U ) X. { 0 } ) ` x ) <-> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) )
51 34 50 bitrdi 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( X |` ( B \ U ) ) = ( ( B \ U ) X. { 0 } ) <-> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) )
52 21 27 51 3bitrd 
 |-  ( ( ph /\ X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) ) -> ( ( ( B \ U ) X. { 0 } ) C_ X <-> A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) )
53 52 pm5.32da 
 |-  ( ph -> ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ ( ( B \ U ) X. { 0 } ) C_ X ) <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )
54 7 53 bitrd 
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. U ) ) ) )