dchrghm - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dchrghm		Structured version Visualization version GIF version

Theorem dchrghm 27431

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
dchrghm	⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀))

Proof of Theorem dchrghm Dummy variable 𝑥 is distinct from all other variables.

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1569 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∖ cdif 3901 ⊆ wss 3904 {csn 4588 dom cdm 5660 ran crn 5661 ↾ cres 5662 “ cima 5663 Fun wfun 6530 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 0cc0 11106 ℕcn 12239 ℕ₀cn0 12510 Basecbs 17275 ↾_s cress 17296 MndHom cmhm 18845 SubMndcsubmnd 18846 Grpcgrp 19006 GrpHom cghm 19289 Abelcabl 19857 mulGrpcmgp 20222 Ringcrg 20321 CRingccrg 20322 Unitcui 20444 ℂ_fldccnfld 21533 ℤ/nℤczn 21663 DChrcdchr 27407

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-addf 11185 ax-mulf 11186

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-tpos 8220 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-er 8692 df-ec 8694 df-qs 8698 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9400 df-inf 9401 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12869 df-fz 13542 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-0g 17500 df-imas 17568 df-qus 17569 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-mhm 18847 df-submnd 18848 df-grp 19009 df-minusg 19010 df-sbg 19011 df-subg 19195 df-nsg 19196 df-eqg 19197 df-ghm 19290 df-cmn 19858 df-abl 19859 df-mgp 20223 df-rng 20237 df-ur 20270 df-ring 20323 df-cring 20324 df-oppr 20426 df-dvdsr 20446 df-unit 20447 df-invr 20477 df-dvr 20490 df-subrng 20656 df-subrg 20680 df-drng 20840 df-lmod 20994 df-lss 21064 df-lsp 21104 df-sra 21305 df-rgmod 21306 df-lidl 21343 df-rsp 21344 df-2idl 21400 df-cnfld 21534 df-zring 21608 df-zn 21667 df-dchr 27408

This theorem is used by: dchrabs 27435 sum2dchr 27449

W3C validator