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 = /N
dchrval.b B = Base Z
dchrval.u U = Unit Z
dchrval.n φ N
dchrbas.b D = Base G
Assertion dchrelbas2 φ X D X mulGrp Z MndHom mulGrp fld 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 dchrelbas φ X D X mulGrp Z MndHom mulGrp fld B U × 0 X
8 eqid mulGrp Z = mulGrp Z
9 8 3 mgpbas B = Base mulGrp Z
10 eqid mulGrp fld = mulGrp fld
11 cnfldbas = Base fld
12 10 11 mgpbas = Base mulGrp fld
13 9 12 mhmf X mulGrp Z MndHom mulGrp fld X : B
14 13 adantl φ X mulGrp Z MndHom mulGrp fld X : B
15 14 ffund φ X mulGrp Z MndHom mulGrp fld Fun X
16 funssres Fun X B U × 0 X X dom B U × 0 = B U × 0
17 15 16 sylan φ X mulGrp Z MndHom mulGrp fld B U × 0 X X dom B U × 0 = B U × 0
18 simpr φ X mulGrp Z MndHom mulGrp fld X dom B U × 0 = B U × 0 X dom B U × 0 = B U × 0
19 resss X dom B U × 0 X
20 18 19 eqsstrrdi φ X mulGrp Z MndHom mulGrp fld X dom B U × 0 = B U × 0 B U × 0 X
21 17 20 impbida φ X mulGrp Z MndHom mulGrp fld B U × 0 X X dom B U × 0 = B U × 0
22 0cn 0
23 fconst6g 0 B U × 0 : B U
24 22 23 mp1i φ X mulGrp Z MndHom mulGrp fld B U × 0 : B U
25 24 fdmd φ X mulGrp Z MndHom mulGrp fld dom B U × 0 = B U
26 25 reseq2d φ X mulGrp Z MndHom mulGrp fld X dom B U × 0 = X B U
27 26 eqeq1d φ X mulGrp Z MndHom mulGrp fld X dom B U × 0 = B U × 0 X B U = B U × 0
28 difss B U B
29 fssres X : B B U B X B U : B U
30 14 28 29 sylancl φ X mulGrp Z MndHom mulGrp fld X B U : B U
31 30 ffnd φ X mulGrp Z MndHom mulGrp fld X B U Fn B U
32 24 ffnd φ X mulGrp Z MndHom mulGrp fld B U × 0 Fn B U
33 eqfnfv X B U Fn B U B U × 0 Fn B U X B U = B U × 0 x B U X B U x = B U × 0 x
34 31 32 33 syl2anc φ X mulGrp Z MndHom mulGrp fld X B U = B U × 0 x B U X B U x = B U × 0 x
35 fvres x B U X B U x = X x
36 c0ex 0 V
37 36 fvconst2 x B U B U × 0 x = 0
38 35 37 eqeq12d x B U X B U x = B U × 0 x X x = 0
39 38 ralbiia x B U X B U x = B U × 0 x x B U X x = 0
40 eldif x B U x B ¬ x U
41 40 imbi1i x B U X x = 0 x B ¬ x U X x = 0
42 impexp x B ¬ x U X x = 0 x B ¬ x U X x = 0
43 con1b ¬ x U X x = 0 ¬ X x = 0 x U
44 df-ne X x 0 ¬ X x = 0
45 44 imbi1i X x 0 x U ¬ X x = 0 x U
46 43 45 bitr4i ¬ x U X x = 0 X x 0 x U
47 46 imbi2i x B ¬ x U X x = 0 x B X x 0 x U
48 41 42 47 3bitri x B U X x = 0 x B X x 0 x U
49 48 ralbii2 x B U X x = 0 x B X x 0 x U
50 39 49 bitri x B U X B U x = B U × 0 x x B X x 0 x U
51 34 50 bitrdi φ X mulGrp Z MndHom mulGrp fld X B U = B U × 0 x B X x 0 x U
52 21 27 51 3bitrd φ X mulGrp Z MndHom mulGrp fld B U × 0 X x B X x 0 x U
53 52 pm5.32da φ X mulGrp Z MndHom mulGrp fld B U × 0 X X mulGrp Z MndHom mulGrp fld x B X x 0 x U
54 7 53 bitrd φ X D X mulGrp Z MndHom mulGrp fld x B X x 0 x U