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 27584

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 27569	. . . . 5 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
5		dchrghm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
6	4, 5	sselid 3906	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
7	1, 3	dchrrcl 27568	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
8	5, 7	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9	8	nnnn0d 12668	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
10	2	zncrng 21851	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
11	9, 10	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ CRing)
12		crngring 20473	. . . . . 6 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
13	11, 12	syl 18	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ Ring)
14		dchrghm.u	. . . . . 6 ⊢ 𝑈 = (Unit‘𝑍)
15		eqid 2760	. . . . . 6 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
16	14, 15	unitsubm 20617	. . . . 5 ⊢ (𝑍 ∈ Ring → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
17	13, 16	syl 18	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
18		dchrghm.h	. . . . 5 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
19	18	resmhm 19017	. . . 4 ⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) ∧ 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍))) → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
20	6, 17, 19	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
21		cnring 21701	. . . . 5 ⊢ ℂ_fld ∈ Ring
22		cnfldbas 21683	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
23		cnfld0 21703	. . . . . . 7 ⊢ 0 = (0_g‘ℂ_fld)
24		cndrng 21708	. . . . . . 7 ⊢ ℂ_fld ∈ DivRing
25	22, 23, 24	drngui 20987	. . . . . 6 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
26		eqid 2760	. . . . . 6 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
27	25, 26	unitsubm 20617	. . . . 5 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
28	21, 27	ax-mp 5	. . . 4 ⊢ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld))
29		df-ima 5663	. . . . 5 ⊢ (𝑋 “ 𝑈) = ran (𝑋 ↾ 𝑈)
30		eqid 2760	. . . . . . . . . 10 ⊢ (Base‘𝑍) = (Base‘𝑍)
31	1, 2, 3, 30, 5	dchrf 27570	. . . . . . . . 9 ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ)
32	30, 14	unitss 20607	. . . . . . . . . 10 ⊢ 𝑈 ⊆ (Base‘𝑍)
33	32	sseli 3904	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑍))
34		ffvelcdm 7081	. . . . . . . . 9 ⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℂ)
35	31, 33, 34	syl2an 608	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ∈ ℂ)
36		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈)
37	5	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑋 ∈ 𝐷)
38	33	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑍))
39	1, 2, 3, 30, 14, 37, 38	dchrn0 27578	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → ((𝑋‘𝑥) ≠ 0 ↔ 𝑥 ∈ 𝑈))
40	36, 39	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ≠ 0)
41		eldifsn 4747	. . . . . . . 8 ⊢ ((𝑋‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝑋‘𝑥) ∈ ℂ ∧ (𝑋‘𝑥) ≠ 0))
42	35, 40, 41	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
43	42	ralrimiva 3154	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
44	31	ffund 6714	. . . . . . 7 ⊢ (𝜑 → Fun 𝑋)
45	31	fdmd 6720	. . . . . . . 8 ⊢ (𝜑 → dom 𝑋 = (Base‘𝑍))
46	32, 45	sseqtrrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ dom 𝑋)
47		funimass4 6949	. . . . . . 7 ⊢ ((Fun 𝑋 ∧ 𝑈 ⊆ dom 𝑋) → ((𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}) ↔ ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0})))
48	44, 46, 47	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}) ↔ ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0})))
49	43, 48	mpbird 260	. . . . 5 ⊢ (𝜑 → (𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}))
50	29, 49	eqsstrrid 3947	. . . 4 ⊢ (𝜑 → ran (𝑋 ↾ 𝑈) ⊆ (ℂ ∖ {0}))
51		dchrghm.m	. . . . 5 ⊢ 𝑀 = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
52	51	resmhm2b 19019	. . . 4 ⊢ (((ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ran (𝑋 ↾ 𝑈) ⊆ (ℂ ∖ {0})) → ((𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)) ↔ (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀)))
53	28, 50, 52	sylancr 599	. . 3 ⊢ (𝜑 → ((𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)) ↔ (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀)))
54	20, 53	mpbid 235	. 2 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀))
55	14, 18	unitgrp 20614	. . . 4 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
56	13, 55	syl 18	. . 3 ⊢ (𝜑 → 𝐻 ∈ Grp)
57	51	cnmgpabl 21735	. . . 4 ⊢ 𝑀 ∈ Abel
58		ablgrp 20000	. . . 4 ⊢ (𝑀 ∈ Abel → 𝑀 ∈ Grp)
59	57, 58	ax-mp 5	. . 3 ⊢ 𝑀 ∈ Grp
60		ghmmhmb 19442	. . 3 ⊢ ((𝐻 ∈ Grp ∧ 𝑀 ∈ Grp) → (𝐻 GrpHom 𝑀) = (𝐻 MndHom 𝑀))
61	56, 59, 60	sylancl 598	. 2 ⊢ (𝜑 → (𝐻 GrpHom 𝑀) = (𝐻 MndHom 𝑀))
62	54, 61	eleqtrrd 2863	1 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∀wral 3076 ⊆ wss 3895 ∖ cdif 4045 {csn 4583 dom cdm 5650 ran crn 5651 ↾ cres 5652 “ cima 5653 Fun wfun 6532 ⟶wf 6534 ‘cfv 6538 (class class class)co 7420 ℂcc 11199 0cc0 11201 ℕcn 12336 ℕ₀cn0 12607 Basecbs 17388 ↾_s cress 17409 MndHom cmhm 18977 SubMndcsubmnd 18978 Grpcgrp 19145 GrpHom cghm 19428 Abelcabl 19996 mulGrpcmgp 20361 Ringcrg 20460 CRingccrg 20461 Unitcui 20586 ℂ_fldccnfld 21679 ℤ/nℤczn 21809 DChrcdchr 27560

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11257 ax-resscn 11258 ax-1cn 11259 ax-icn 11260 ax-addcl 11261 ax-addrcl 11262 ax-mulcl 11263 ax-mulrcl 11264 ax-mulcom 11265 ax-addass 11266 ax-mulass 11267 ax-distr 11268 ax-i2m1 11269 ax-1ne0 11270 ax-1rid 11271 ax-rnegex 11272 ax-rrecex 11273 ax-cnre 11274 ax-pre-lttri 11275 ax-pre-lttrn 11276 ax-pre-ltadd 11277 ax-pre-mulgt0 11278 ax-addf 11280 ax-mulf 11281

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-tpos 8244 df-frecs 8300 df-wrecs 8331 df-recs 8380 df-rdg 8419 df-1o 8477 df-er 8718 df-ec 8720 df-qs 8724 df-map 8850 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9435 df-inf 9436 df-pnf 11346 df-mnf 11347 df-xr 11348 df-ltxr 11349 df-le 11350 df-sub 11544 df-neg 11545 df-div 11975 df-nn 12337 df-2 12406 df-3 12407 df-4 12408 df-5 12409 df-6 12410 df-7 12411 df-8 12412 df-9 12413 df-n0 12608 df-z 12695 df-dec 12816 df-uz 12967 df-fz 13641 df-struct 17326 df-sets 17343 df-slot 17361 df-ndx 17373 df-base 17389 df-ress 17410 df-plusg 17442 df-mulr 17443 df-starv 17444 df-sca 17445 df-vsca 17446 df-ip 17447 df-tset 17448 df-ple 17449 df-ds 17451 df-unif 17452 df-0g 17613 df-imas 17681 df-qus 17682 df-mgm 18817 df-sgrp 18909 df-mnd 18925 df-mhm 18979 df-submnd 18980 df-grp 19148 df-minusg 19149 df-sbg 19150 df-subg 19334 df-nsg 19335 df-eqg 19336 df-ghm 19429 df-cmn 19997 df-abl 19998 df-mgp 20362 df-rng 20376 df-ur 20409 df-ring 20462 df-cring 20463 df-oppr 20568 df-dvdsr 20588 df-unit 20589 df-invr 20619 df-dvr 20632 df-subrng 20799 df-subrg 20823 df-drng 20983 df-lmod 21138 df-lss 21208 df-lsp 21248 df-sra 21449 df-rgmod 21450 df-lidl 21487 df-rsp 21488 df-2idl 21544 df-cnfld 21680 df-zring 21754 df-zn 21813 df-dchr 27561

This theorem is used by: dchrabs 27588 sum2dchr 27602

W3C validator