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	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrghm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrghm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrghm.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrghm.h	⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾_s 𝑈 )
	dchrghm.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂ_fld ) ↾_s ( ℂ ∖ { 0 } ) )
	dchrghm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	dchrghm	⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 GrpHom 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		dchrghm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrghm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrghm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrghm.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
5		dchrghm.h	⊢ 𝐻 = ( ( mulGrp ‘ 𝑍 ) ↾_s 𝑈 )
6		dchrghm.m	⊢ 𝑀 = ( ( mulGrp ‘ ℂ_fld ) ↾_s ( ℂ ∖ { 0 } ) )
7		dchrghm.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8	1 2 3	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂ_fld ) )
9	8 7	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂ_fld ) ) )
10	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
11	7 10	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12	11	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
13	2	zncrng	⊢ ( 𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing )
14	12 13	syl	⊢ ( 𝜑 → 𝑍 ∈ CRing )
15		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
16	14 15	syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
17		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
18	4 17	unitsubm	⊢ ( 𝑍 ∈ Ring → 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) )
19	16 18	syl	⊢ ( 𝜑 → 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) )
20	5	resmhm	⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂ_fld ) ) ∧ 𝑈 ∈ ( SubMnd ‘ ( mulGrp ‘ 𝑍 ) ) ) → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂ_fld ) ) )
21	9 19 20	syl2anc	⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂ_fld ) ) )
22		cnring	⊢ ℂ_fld ∈ Ring
23		cnfldbas	⊢ ℂ = ( Base ‘ ℂ_fld )
24		cnfld0	⊢ 0 = ( 0_g ‘ ℂ_fld )
25		cndrng	⊢ ℂ_fld ∈ DivRing
26	23 24 25	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂ_fld )
27		eqid	⊢ ( mulGrp ‘ ℂ_fld ) = ( mulGrp ‘ ℂ_fld )
28	26 27	unitsubm	⊢ ( ℂ_fld ∈ Ring → ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂ_fld ) ) )
29	22 28	ax-mp	⊢ ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂ_fld ) )
30		df-ima	⊢ ( 𝑋 “ 𝑈 ) = ran ( 𝑋 ↾ 𝑈 )
31		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
32	1 2 3 31 7	dchrf	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
33	31 4	unitss	⊢ 𝑈 ⊆ ( Base ‘ 𝑍 )
34	33	sseli	⊢ ( 𝑥 ∈ 𝑈 → 𝑥 ∈ ( Base ‘ 𝑍 ) )
35		ffvelcdm	⊢ ( ( 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ ∧ 𝑥 ∈ ( Base ‘ 𝑍 ) ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
36	32 34 35	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ∈ ℂ )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ 𝑈 )
38	7	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑋 ∈ 𝐷 )
39	34	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → 𝑥 ∈ ( Base ‘ 𝑍 ) )
40	1 2 3 31 4 38 39	dchrn0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ 𝑥 ∈ 𝑈 ) )
41	37 40	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ≠ 0 )
42		eldifsn	⊢ ( ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑋 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝑋 ‘ 𝑥 ) ≠ 0 ) )
43	36 41 42	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑈 ) → ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
44	43	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) )
45	32	ffund	⊢ ( 𝜑 → Fun 𝑋 )
46	32	fdmd	⊢ ( 𝜑 → dom 𝑋 = ( Base ‘ 𝑍 ) )
47	33 46	sseqtrrid	⊢ ( 𝜑 → 𝑈 ⊆ dom 𝑋 )
48		funimass4	⊢ ( ( Fun 𝑋 ∧ 𝑈 ⊆ dom 𝑋 ) → ( ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
49	45 47 48	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ↔ ∀ 𝑥 ∈ 𝑈 ( 𝑋 ‘ 𝑥 ) ∈ ( ℂ ∖ { 0 } ) ) )
50	44 49	mpbird	⊢ ( 𝜑 → ( 𝑋 “ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) )
51	30 50	eqsstrrid	⊢ ( 𝜑 → ran ( 𝑋 ↾ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) )
52	6	resmhm2b	⊢ ( ( ( ℂ ∖ { 0 } ) ∈ ( SubMnd ‘ ( mulGrp ‘ ℂ_fld ) ) ∧ ran ( 𝑋 ↾ 𝑈 ) ⊆ ( ℂ ∖ { 0 } ) ) → ( ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂ_fld ) ) ↔ ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) ) )
53	29 51 52	sylancr	⊢ ( 𝜑 → ( ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom ( mulGrp ‘ ℂ_fld ) ) ↔ ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) ) )
54	21 53	mpbid	⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 MndHom 𝑀 ) )
55	4 5	unitgrp	⊢ ( 𝑍 ∈ Ring → 𝐻 ∈ Grp )
56	16 55	syl	⊢ ( 𝜑 → 𝐻 ∈ Grp )
57	6	cnmgpabl	⊢ 𝑀 ∈ Abel
58		ablgrp	⊢ ( 𝑀 ∈ Abel → 𝑀 ∈ Grp )
59	57 58	ax-mp	⊢ 𝑀 ∈ Grp
60		ghmmhmb	⊢ ( ( 𝐻 ∈ Grp ∧ 𝑀 ∈ Grp ) → ( 𝐻 GrpHom 𝑀 ) = ( 𝐻 MndHom 𝑀 ) )
61	56 59 60	sylancl	⊢ ( 𝜑 → ( 𝐻 GrpHom 𝑀 ) = ( 𝐻 MndHom 𝑀 ) )
62	54 61	eleqtrrd	⊢ ( 𝜑 → ( 𝑋 ↾ 𝑈 ) ∈ ( 𝐻 GrpHom 𝑀 ) )

Metamath Proof Explorer

Theorem dchrghm

Proof