dchrghm

Description: A Dirichlet character restricted to the unit group of Z/nZ is a group homomorphism into the multiplicative group of nonzero complex numbers. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	dchrghm.g	$⊢ G = DChr (N)$
	dchrghm.z	$⊢ Z = ℤ / N ℤ$
	dchrghm.b	$⊢ D = {Base}_{G}$
	dchrghm.u	$⊢ U = Unit (Z)$
	dchrghm.h	$⊢ H = {mulGrp}_{Z} ↾_{𝑠} U$
	dchrghm.m	$⊢ M = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
	dchrghm.x	$⊢ φ \to X \in D$
Assertion	dchrghm	$⊢ φ \to {X ↾}_{U} \in (H GrpHom M)$

Proof

Step	Hyp	Ref	Expression
1		dchrghm.g	$⊢ G = DChr (N)$
2		dchrghm.z	$⊢ Z = ℤ / N ℤ$
3		dchrghm.b	$⊢ D = {Base}_{G}$
4		dchrghm.u	$⊢ U = Unit (Z)$
5		dchrghm.h	$⊢ H = {mulGrp}_{Z} ↾_{𝑠} U$
6		dchrghm.m	$⊢ M = {mulGrp}_{ℂ_{fld}} ↾_{𝑠} (ℂ ∖ \{0\})$
7		dchrghm.x	$⊢ φ \to X \in D$
8	1 2 3	dchrmhm	$⊢ D \subseteq {mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}$
9	8 7	sseldi	$⊢ φ \to X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}})$
10	1 3	dchrrcl	$⊢ X \in D \to N \in ℕ$
11	7 10	syl	$⊢ φ \to N \in ℕ$
12	11	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
13	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
14	12 13	syl	$⊢ φ \to Z \in CRing$
15		crngring	$⊢ Z \in CRing \to Z \in Ring$
16	14 15	syl	$⊢ φ \to Z \in Ring$
17		eqid	$⊢ {mulGrp}_{Z} = {mulGrp}_{Z}$
18	4 17	unitsubm	$⊢ Z \in Ring \to U \in SubMnd ({mulGrp}_{Z})$
19	16 18	syl	$⊢ φ \to U \in SubMnd ({mulGrp}_{Z})$
20	5	resmhm	$⊢ (X \in ({mulGrp}_{Z} MndHom {mulGrp}_{ℂ_{fld}}) \land U \in SubMnd ({mulGrp}_{Z})) \to {X ↾}_{U} \in (H MndHom {mulGrp}_{ℂ_{fld}})$
21	9 19 20	syl2anc	$⊢ φ \to {X ↾}_{U} \in (H MndHom {mulGrp}_{ℂ_{fld}})$
22		cnring	$⊢ ℂ_{fld} \in Ring$
23		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
24		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
25		cndrng	$⊢ ℂ_{fld} \in DivRing$
26	23 24 25	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
27		eqid	$⊢ {mulGrp}_{ℂ_{fld}} = {mulGrp}_{ℂ_{fld}}$
28	26 27	unitsubm	$⊢ ℂ_{fld} \in Ring \to ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
29	22 28	ax-mp	$⊢ ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}})$
30		df-ima	$⊢ X [U] = ran ({X ↾}_{U})$
31		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
32	1 2 3 31 7	dchrf	$⊢ φ \to X : {Base}_{Z} ⟶ ℂ$
33	31 4	unitss	$⊢ U \subseteq {Base}_{Z}$
34	33	sseli	$⊢ x \in U \to x \in {Base}_{Z}$
35		ffvelrn	$⊢ (X : {Base}_{Z} ⟶ ℂ \land x \in {Base}_{Z}) \to X (x) \in ℂ$
36	32 34 35	syl2an	$⊢ (φ \land x \in U) \to X (x) \in ℂ$
37		simpr	$⊢ (φ \land x \in U) \to x \in U$
38	7	adantr	$⊢ (φ \land x \in U) \to X \in D$
39	34	adantl	$⊢ (φ \land x \in U) \to x \in {Base}_{Z}$
40	1 2 3 31 4 38 39	dchrn0	$⊢ (φ \land x \in U) \to (X (x) \neq 0 \leftrightarrow x \in U)$
41	37 40	mpbird	$⊢ (φ \land x \in U) \to X (x) \neq 0$
42		eldifsn	$⊢ X (x) \in (ℂ ∖ \{0\}) \leftrightarrow (X (x) \in ℂ \land X (x) \neq 0)$
43	36 41 42	sylanbrc	$⊢ (φ \land x \in U) \to X (x) \in (ℂ ∖ \{0\})$
44	43	ralrimiva	$⊢ φ \to \forall x \in U X (x) \in (ℂ ∖ \{0\})$
45	32	ffund	$⊢ φ \to Fun X$
46	32	fdmd	$⊢ φ \to dom X = {Base}_{Z}$
47	33 46	sseqtrrid	$⊢ φ \to U \subseteq dom X$
48		funimass4	$⊢ (Fun X \land U \subseteq dom X) \to (X [U] \subseteq ℂ ∖ \{0\} \leftrightarrow \forall x \in U X (x) \in (ℂ ∖ \{0\}))$
49	45 47 48	syl2anc	$⊢ φ \to (X [U] \subseteq ℂ ∖ \{0\} \leftrightarrow \forall x \in U X (x) \in (ℂ ∖ \{0\}))$
50	44 49	mpbird	$⊢ φ \to X [U] \subseteq ℂ ∖ \{0\}$
51	30 50	eqsstrrid	$⊢ φ \to ran ({X ↾}_{U}) \subseteq ℂ ∖ \{0\}$
52	6	resmhm2b	$⊢ (ℂ ∖ \{0\} \in SubMnd ({mulGrp}_{ℂ_{fld}}) \land ran ({X ↾}_{U}) \subseteq ℂ ∖ \{0\}) \to ({X ↾}_{U} \in (H MndHom {mulGrp}_{ℂ_{fld}}) \leftrightarrow {X ↾}_{U} \in (H MndHom M))$
53	29 51 52	sylancr	$⊢ φ \to ({X ↾}_{U} \in (H MndHom {mulGrp}_{ℂ_{fld}}) \leftrightarrow {X ↾}_{U} \in (H MndHom M))$
54	21 53	mpbid	$⊢ φ \to {X ↾}_{U} \in (H MndHom M)$
55	4 5	unitgrp	$⊢ Z \in Ring \to H \in Grp$
56	16 55	syl	$⊢ φ \to H \in Grp$
57	6	cnmgpabl	$⊢ M \in Abel$
58		ablgrp	$⊢ M \in Abel \to M \in Grp$
59	57 58	ax-mp	$⊢ M \in Grp$
60		ghmmhmb	$⊢ (H \in Grp \land M \in Grp) \to H GrpHom M = H MndHom M$
61	56 59 60	sylancl	$⊢ φ \to H GrpHom M = H MndHom M$
62	54 61	eleqtrrd	$⊢ φ \to {X ↾}_{U} \in (H GrpHom M)$

Metamath Proof Explorer

Theorem dchrghm

Proof