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