Metamath Proof Explorer

Theorem dchrelbasd

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, 28-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 )
dchrelbasd.1 
|- ( k = x -> X = A )
dchrelbasd.2 
|- ( k = y -> X = C )
dchrelbasd.3 
|- ( k = ( x ( .r ` Z ) y ) -> X = E )
dchrelbasd.4 
|- ( k = ( 1r ` Z ) -> X = Y )
dchrelbasd.5 
|- ( ( ph /\ k e. U ) -> X e. CC )
dchrelbasd.6 
|- ( ( ph /\ ( x e. U /\ y e. U ) ) -> E = ( A x. C ) )
dchrelbasd.7 
|- ( ph -> Y = 1 )
Assertion dchrelbasd 
|- ( ph -> ( k e. B |-> if ( k e. U , X , 0 ) ) e. D )

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 dchrelbasd.1 
 |-  ( k = x -> X = A )
8 dchrelbasd.2 
 |-  ( k = y -> X = C )
9 dchrelbasd.3 
 |-  ( k = ( x ( .r ` Z ) y ) -> X = E )
10 dchrelbasd.4 
 |-  ( k = ( 1r ` Z ) -> X = Y )
11 dchrelbasd.5 
 |-  ( ( ph /\ k e. U ) -> X e. CC )
12 dchrelbasd.6 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> E = ( A x. C ) )
13 dchrelbasd.7 
 |-  ( ph -> Y = 1 )
14 11 adantlr 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> X e. CC )
15 0cnd 
 |-  ( ( ( ph /\ k e. B ) /\ -. k e. U ) -> 0 e. CC )
16 14 15 ifclda 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , X , 0 ) e. CC )
17 16 fmpttd 
 |-  ( ph -> ( k e. B |-> if ( k e. U , X , 0 ) ) : B --> CC )
18 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
19 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
20 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
21 18 19 20 3syl 
 |-  ( ph -> Z e. Ring )
22 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
23 4 22 unitmulcl 
 |-  ( ( Z e. Ring /\ x e. U /\ y e. U ) -> ( x ( .r ` Z ) y ) e. U )
24 23 3expb 
 |-  ( ( Z e. Ring /\ ( x e. U /\ y e. U ) ) -> ( x ( .r ` Z ) y ) e. U )
25 21 24 sylan 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( x ( .r ` Z ) y ) e. U )
26 25 iftrued 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( ( x ( .r ` Z ) y ) e. U , E , 0 ) = E )
27 26 12 eqtrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( ( x ( .r ` Z ) y ) e. U , E , 0 ) = ( A x. C ) )
28 eqid 
 |-  ( k e. B |-> if ( k e. U , X , 0 ) ) = ( k e. B |-> if ( k e. U , X , 0 ) )
29 eleq1 
 |-  ( k = ( x ( .r ` Z ) y ) -> ( k e. U <-> ( x ( .r ` Z ) y ) e. U ) )
30 29 9 ifbieq1d 
 |-  ( k = ( x ( .r ` Z ) y ) -> if ( k e. U , X , 0 ) = if ( ( x ( .r ` Z ) y ) e. U , E , 0 ) )
31 3 4 unitss 
 |-  U C_ B
32 31 25 sselid 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( x ( .r ` Z ) y ) e. B )
33 9 eleq1d 
 |-  ( k = ( x ( .r ` Z ) y ) -> ( X e. CC <-> E e. CC ) )
34 11 ralrimiva 
 |-  ( ph -> A. k e. U X e. CC )
35 34 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> A. k e. U X e. CC )
36 33 35 25 rspcdva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> E e. CC )
37 26 36 eqeltrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( ( x ( .r ` Z ) y ) e. U , E , 0 ) e. CC )
38 28 30 32 37 fvmptd3 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( x ( .r ` Z ) y ) ) = if ( ( x ( .r ` Z ) y ) e. U , E , 0 ) )
39 eleq1 
 |-  ( k = x -> ( k e. U <-> x e. U ) )
40 39 7 ifbieq1d 
 |-  ( k = x -> if ( k e. U , X , 0 ) = if ( x e. U , A , 0 ) )
41 simprl 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. U )
42 31 41 sselid 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. B )
43 iftrue 
 |-  ( x e. U -> if ( x e. U , A , 0 ) = A )
44 43 ad2antrl 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( x e. U , A , 0 ) = A )
45 7 eleq1d 
 |-  ( k = x -> ( X e. CC <-> A e. CC ) )
46 45 35 41 rspcdva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> A e. CC )
47 44 46 eqeltrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( x e. U , A , 0 ) e. CC )
48 28 40 42 47 fvmptd3 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) = if ( x e. U , A , 0 ) )
49 48 44 eqtrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) = A )
50 eleq1 
 |-  ( k = y -> ( k e. U <-> y e. U ) )
51 50 8 ifbieq1d 
 |-  ( k = y -> if ( k e. U , X , 0 ) = if ( y e. U , C , 0 ) )
52 simprr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. U )
53 31 52 sselid 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. B )
54 iftrue 
 |-  ( y e. U -> if ( y e. U , C , 0 ) = C )
55 54 ad2antll 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( y e. U , C , 0 ) = C )
56 8 eleq1d 
 |-  ( k = y -> ( X e. CC <-> C e. CC ) )
57 56 35 52 rspcdva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> C e. CC )
58 55 57 eqeltrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> if ( y e. U , C , 0 ) e. CC )
59 28 51 53 58 fvmptd3 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) = if ( y e. U , C , 0 ) )
60 59 55 eqtrd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) = C )
61 49 60 oveq12d 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) x. ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) ) = ( A x. C ) )
62 27 38 61 3eqtr4d 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( x ( .r ` Z ) y ) ) = ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) x. ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) ) )
63 62 ralrimivva 
 |-  ( ph -> A. x e. U A. y e. U ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( x ( .r ` Z ) y ) ) = ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) x. ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) ) )
64 eleq1 
 |-  ( k = ( 1r ` Z ) -> ( k e. U <-> ( 1r ` Z ) e. U ) )
65 64 10 ifbieq1d 
 |-  ( k = ( 1r ` Z ) -> if ( k e. U , X , 0 ) = if ( ( 1r ` Z ) e. U , Y , 0 ) )
66 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
67 4 66 1unit 
 |-  ( Z e. Ring -> ( 1r ` Z ) e. U )
68 21 67 syl 
 |-  ( ph -> ( 1r ` Z ) e. U )
69 31 68 sselid 
 |-  ( ph -> ( 1r ` Z ) e. B )
70 68 iftrued 
 |-  ( ph -> if ( ( 1r ` Z ) e. U , Y , 0 ) = Y )
71 70 13 eqtrd 
 |-  ( ph -> if ( ( 1r ` Z ) e. U , Y , 0 ) = 1 )
72 ax-1cn 
 |-  1 e. CC
73 71 72 eqeltrdi 
 |-  ( ph -> if ( ( 1r ` Z ) e. U , Y , 0 ) e. CC )
74 28 65 69 73 fvmptd3 
 |-  ( ph -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( 1r ` Z ) ) = if ( ( 1r ` Z ) e. U , Y , 0 ) )
75 74 71 eqtrd 
 |-  ( ph -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( 1r ` Z ) ) = 1 )
76 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
77 45 rspcv 
 |-  ( x e. U -> ( A. k e. U X e. CC -> A e. CC ) )
78 34 77 mpan9 
 |-  ( ( ph /\ x e. U ) -> A e. CC )
79 78 adantlr 
 |-  ( ( ( ph /\ x e. B ) /\ x e. U ) -> A e. CC )
80 0cnd 
 |-  ( ( ( ph /\ x e. B ) /\ -. x e. U ) -> 0 e. CC )
81 79 80 ifclda 
 |-  ( ( ph /\ x e. B ) -> if ( x e. U , A , 0 ) e. CC )
82 28 40 76 81 fvmptd3 
 |-  ( ( ph /\ x e. B ) -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) = if ( x e. U , A , 0 ) )
83 82 neeq1d 
 |-  ( ( ph /\ x e. B ) -> ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) =/= 0 <-> if ( x e. U , A , 0 ) =/= 0 ) )
84 iffalse 
 |-  ( -. x e. U -> if ( x e. U , A , 0 ) = 0 )
85 84 necon1ai 
 |-  ( if ( x e. U , A , 0 ) =/= 0 -> x e. U )
86 83 85 syl6bi 
 |-  ( ( ph /\ x e. B ) -> ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) =/= 0 -> x e. U ) )
87 86 ralrimiva 
 |-  ( ph -> A. x e. B ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) =/= 0 -> x e. U ) )
88 63 75 87 3jca 
 |-  ( ph -> ( A. x e. U A. y e. U ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( x ( .r ` Z ) y ) ) = ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) x. ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) ) /\ ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) =/= 0 -> x e. U ) ) )
89 1 2 3 4 5 6 dchrelbas3 
 |-  ( ph -> ( ( k e. B |-> if ( k e. U , X , 0 ) ) e. D <-> ( ( k e. B |-> if ( k e. U , X , 0 ) ) : B --> CC /\ ( A. x e. U A. y e. U ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( x ( .r ` Z ) y ) ) = ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) x. ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` y ) ) /\ ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( ( k e. B |-> if ( k e. U , X , 0 ) ) ` x ) =/= 0 -> x e. U ) ) ) ) )
90 17 88 89 mpbir2and 
 |-  ( ph -> ( k e. B |-> if ( k e. U , X , 0 ) ) e. D )