Metamath Proof Explorer


Theorem dchrelbas3

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, 19-Apr-2016)

Ref Expression
Hypotheses dchrval.g G = DChr N
dchrval.z Z = /N
dchrval.b B = Base Z
dchrval.u U = Unit Z
dchrval.n φ N
dchrbas.b D = Base G
Assertion dchrelbas3 φ X D X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U

Proof

Step Hyp Ref Expression
1 dchrval.g G = DChr N
2 dchrval.z Z = /N
3 dchrval.b B = Base Z
4 dchrval.u U = Unit Z
5 dchrval.n φ N
6 dchrbas.b D = Base G
7 1 2 3 4 5 6 dchrelbas2 φ X D X mulGrp Z MndHom mulGrp fld x B X x 0 x U
8 fveq2 z = x X z = X x
9 8 neeq1d z = x X z 0 X x 0
10 eleq1 z = x z U x U
11 9 10 imbi12d z = x X z 0 z U X x 0 x U
12 11 cbvralvw z B X z 0 z U x B X x 0 x U
13 5 nnnn0d φ N 0
14 2 zncrng N 0 Z CRing
15 13 14 syl φ Z CRing
16 crngring Z CRing Z Ring
17 15 16 syl φ Z Ring
18 eqid mulGrp Z = mulGrp Z
19 18 ringmgp Z Ring mulGrp Z Mnd
20 17 19 syl φ mulGrp Z Mnd
21 cnring fld Ring
22 eqid mulGrp fld = mulGrp fld
23 22 ringmgp fld Ring mulGrp fld Mnd
24 21 23 ax-mp mulGrp fld Mnd
25 18 3 mgpbas B = Base mulGrp Z
26 cnfldbas = Base fld
27 22 26 mgpbas = Base mulGrp fld
28 eqid Z = Z
29 18 28 mgpplusg Z = + mulGrp Z
30 cnfldmul × = fld
31 22 30 mgpplusg × = + mulGrp fld
32 eqid 1 Z = 1 Z
33 18 32 ringidval 1 Z = 0 mulGrp Z
34 cnfld1 1 = 1 fld
35 22 34 ringidval 1 = 0 mulGrp fld
36 25 27 29 31 33 35 ismhm X mulGrp Z MndHom mulGrp fld mulGrp Z Mnd mulGrp fld Mnd X : B x B y B X x Z y = X x X y X 1 Z = 1
37 36 baib mulGrp Z Mnd mulGrp fld Mnd X mulGrp Z MndHom mulGrp fld X : B x B y B X x Z y = X x X y X 1 Z = 1
38 20 24 37 sylancl φ X mulGrp Z MndHom mulGrp fld X : B x B y B X x Z y = X x X y X 1 Z = 1
39 38 adantr φ z B X z 0 z U X mulGrp Z MndHom mulGrp fld X : B x B y B X x Z y = X x X y X 1 Z = 1
40 biimt x U y U X x Z y = X x X y x U y U X x Z y = X x X y
41 40 adantl φ z B X z 0 z U X : B x B y B x U y U X x Z y = X x X y x U y U X x Z y = X x X y
42 fveq2 z = x Z y X z = X x Z y
43 42 neeq1d z = x Z y X z 0 X x Z y 0
44 eleq1 z = x Z y z U x Z y U
45 43 44 imbi12d z = x Z y X z 0 z U X x Z y 0 x Z y U
46 simpllr φ z B X z 0 z U X : B x B y B z B X z 0 z U
47 17 ad3antrrr φ z B X z 0 z U X : B x B y B Z Ring
48 simprl φ z B X z 0 z U X : B x B y B x B
49 simprr φ z B X z 0 z U X : B x B y B y B
50 3 28 ringcl Z Ring x B y B x Z y B
51 47 48 49 50 syl3anc φ z B X z 0 z U X : B x B y B x Z y B
52 45 46 51 rspcdva φ z B X z 0 z U X : B x B y B X x Z y 0 x Z y U
53 15 ad3antrrr φ z B X z 0 z U X : B x B y B Z CRing
54 4 28 3 unitmulclb Z CRing x B y B x Z y U x U y U
55 53 48 49 54 syl3anc φ z B X z 0 z U X : B x B y B x Z y U x U y U
56 52 55 sylibd φ z B X z 0 z U X : B x B y B X x Z y 0 x U y U
57 56 necon1bd φ z B X z 0 z U X : B x B y B ¬ x U y U X x Z y = 0
58 57 imp φ z B X z 0 z U X : B x B y B ¬ x U y U X x Z y = 0
59 11 46 48 rspcdva φ z B X z 0 z U X : B x B y B X x 0 x U
60 fveq2 z = y X z = X y
61 60 neeq1d z = y X z 0 X y 0
62 eleq1 z = y z U y U
63 61 62 imbi12d z = y X z 0 z U X y 0 y U
64 63 46 49 rspcdva φ z B X z 0 z U X : B x B y B X y 0 y U
65 59 64 anim12d φ z B X z 0 z U X : B x B y B X x 0 X y 0 x U y U
66 65 con3dimp φ z B X z 0 z U X : B x B y B ¬ x U y U ¬ X x 0 X y 0
67 neanior X x 0 X y 0 ¬ X x = 0 X y = 0
68 67 con2bii X x = 0 X y = 0 ¬ X x 0 X y 0
69 66 68 sylibr φ z B X z 0 z U X : B x B y B ¬ x U y U X x = 0 X y = 0
70 simplr φ z B X z 0 z U X : B x B y B X : B
71 70 48 ffvelrnd φ z B X z 0 z U X : B x B y B X x
72 70 49 ffvelrnd φ z B X z 0 z U X : B x B y B X y
73 71 72 mul0ord φ z B X z 0 z U X : B x B y B X x X y = 0 X x = 0 X y = 0
74 73 adantr φ z B X z 0 z U X : B x B y B ¬ x U y U X x X y = 0 X x = 0 X y = 0
75 69 74 mpbird φ z B X z 0 z U X : B x B y B ¬ x U y U X x X y = 0
76 58 75 eqtr4d φ z B X z 0 z U X : B x B y B ¬ x U y U X x Z y = X x X y
77 76 a1d φ z B X z 0 z U X : B x B y B ¬ x U y U x U y U X x Z y = X x X y
78 76 77 2thd φ z B X z 0 z U X : B x B y B ¬ x U y U X x Z y = X x X y x U y U X x Z y = X x X y
79 41 78 pm2.61dan φ z B X z 0 z U X : B x B y B X x Z y = X x X y x U y U X x Z y = X x X y
80 79 pm5.74da φ z B X z 0 z U X : B x B y B X x Z y = X x X y x B y B x U y U X x Z y = X x X y
81 3 4 unitcl x U x B
82 3 4 unitcl y U y B
83 81 82 anim12i x U y U x B y B
84 83 pm4.71ri x U y U x B y B x U y U
85 84 imbi1i x U y U X x Z y = X x X y x B y B x U y U X x Z y = X x X y
86 impexp x B y B x U y U X x Z y = X x X y x B y B x U y U X x Z y = X x X y
87 85 86 bitri x U y U X x Z y = X x X y x B y B x U y U X x Z y = X x X y
88 80 87 bitr4di φ z B X z 0 z U X : B x B y B X x Z y = X x X y x U y U X x Z y = X x X y
89 88 2albidv φ z B X z 0 z U X : B x y x B y B X x Z y = X x X y x y x U y U X x Z y = X x X y
90 r2al x B y B X x Z y = X x X y x y x B y B X x Z y = X x X y
91 r2al x U y U X x Z y = X x X y x y x U y U X x Z y = X x X y
92 89 90 91 3bitr4g φ z B X z 0 z U X : B x B y B X x Z y = X x X y x U y U X x Z y = X x X y
93 92 adantrr φ z B X z 0 z U X : B X 1 Z = 1 x B y B X x Z y = X x X y x U y U X x Z y = X x X y
94 93 pm5.32da φ z B X z 0 z U X : B X 1 Z = 1 x B y B X x Z y = X x X y X : B X 1 Z = 1 x U y U X x Z y = X x X y
95 3anan32 X : B x B y B X x Z y = X x X y X 1 Z = 1 X : B X 1 Z = 1 x B y B X x Z y = X x X y
96 an31 x U y U X x Z y = X x X y X 1 Z = 1 X : B X : B X 1 Z = 1 x U y U X x Z y = X x X y
97 94 95 96 3bitr4g φ z B X z 0 z U X : B x B y B X x Z y = X x X y X 1 Z = 1 x U y U X x Z y = X x X y X 1 Z = 1 X : B
98 39 97 bitrd φ z B X z 0 z U X mulGrp Z MndHom mulGrp fld x U y U X x Z y = X x X y X 1 Z = 1 X : B
99 12 98 sylan2br φ x B X x 0 x U X mulGrp Z MndHom mulGrp fld x U y U X x Z y = X x X y X 1 Z = 1 X : B
100 99 pm5.32da φ x B X x 0 x U X mulGrp Z MndHom mulGrp fld x B X x 0 x U x U y U X x Z y = X x X y X 1 Z = 1 X : B
101 ancom X mulGrp Z MndHom mulGrp fld x B X x 0 x U x B X x 0 x U X mulGrp Z MndHom mulGrp fld
102 df-3an x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U
103 102 anbi2i X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U
104 an13 X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U x B X x 0 x U x U y U X x Z y = X x X y X 1 Z = 1 X : B
105 103 104 bitri X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U x B X x 0 x U x U y U X x Z y = X x X y X 1 Z = 1 X : B
106 100 101 105 3bitr4g φ X mulGrp Z MndHom mulGrp fld x B X x 0 x U X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U
107 7 106 bitrd φ X D X : B x U y U X x Z y = X x X y X 1 Z = 1 x B X x 0 x U