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 | |
|
dchrval.z | |
||
dchrval.b | |
||
dchrval.u | |
||
dchrval.n | |
||
dchrbas.b | |
||
Assertion | dchrelbas2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dchrval.g | |
|
2 | dchrval.z | |
|
3 | dchrval.b | |
|
4 | dchrval.u | |
|
5 | dchrval.n | |
|
6 | dchrbas.b | |
|
7 | 1 2 3 4 5 6 | dchrelbas | |
8 | eqid | |
|
9 | 8 3 | mgpbas | |
10 | eqid | |
|
11 | cnfldbas | |
|
12 | 10 11 | mgpbas | |
13 | 9 12 | mhmf | |
14 | 13 | adantl | |
15 | 14 | ffund | |
16 | funssres | |
|
17 | 15 16 | sylan | |
18 | simpr | |
|
19 | resss | |
|
20 | 18 19 | eqsstrrdi | |
21 | 17 20 | impbida | |
22 | 0cn | |
|
23 | fconst6g | |
|
24 | 22 23 | mp1i | |
25 | 24 | fdmd | |
26 | 25 | reseq2d | |
27 | 26 | eqeq1d | |
28 | difss | |
|
29 | fssres | |
|
30 | 14 28 29 | sylancl | |
31 | 30 | ffnd | |
32 | 24 | ffnd | |
33 | eqfnfv | |
|
34 | 31 32 33 | syl2anc | |
35 | fvres | |
|
36 | c0ex | |
|
37 | 36 | fvconst2 | |
38 | 35 37 | eqeq12d | |
39 | 38 | ralbiia | |
40 | eldif | |
|
41 | 40 | imbi1i | |
42 | impexp | |
|
43 | con1b | |
|
44 | df-ne | |
|
45 | 44 | imbi1i | |
46 | 43 45 | bitr4i | |
47 | 46 | imbi2i | |
48 | 41 42 47 | 3bitri | |
49 | 48 | ralbii2 | |
50 | 39 49 | bitri | |
51 | 34 50 | bitrdi | |
52 | 21 27 51 | 3bitrd | |
53 | 52 | pm5.32da | |
54 | 7 53 | bitrd | |