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 27493

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 27478	. . . . 5 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
5		dchrghm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
6	4, 5	sselid 3932	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
7	1, 3	dchrrcl 27477	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
8	5, 7	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9	8	nnnn0d 12592	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
10	2	zncrng 21761	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
11	9, 10	syl 18	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ CRing)
12		crngring 20388	. . . . . 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 20531	. . . . 5 ⊢ (𝑍 ∈ Ring → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
17	13, 16	syl 18	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
18		dchrghm.h	. . . . 5 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
19	18	resmhm 18933	. . . 4 ⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) ∧ 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍))) → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
20	6, 17, 19	syl2anc 596	. . 3 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
21		cnring 21611	. . . . 5 ⊢ ℂ_fld ∈ Ring
22		cnfldbas 21593	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
23		cnfld0 21613	. . . . . . 7 ⊢ 0 = (0_g‘ℂ_fld)
24		cndrng 21618	. . . . . . 7 ⊢ ℂ_fld ∈ DivRing
25	22, 23, 24	drngui 20900	. . . . . 6 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
26		eqid 2762	. . . . . 6 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
27	25, 26	unitsubm 20531	. . . . 5 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
28	21, 27	ax-mp 5	. . . 4 ⊢ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld))
29		df-ima 5672	. . . . 5 ⊢ (𝑋 “ 𝑈) = ran (𝑋 ↾ 𝑈)
30		eqid 2762	. . . . . . . . . 10 ⊢ (Base‘𝑍) = (Base‘𝑍)
31	1, 2, 3, 30, 5	dchrf 27479	. . . . . . . . 9 ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ)
32	30, 14	unitss 20521	. . . . . . . . . 10 ⊢ 𝑈 ⊆ (Base‘𝑍)
33	32	sseli 3930	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑍))
34		ffvelcdm 7077	. . . . . . . . 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 27487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → ((𝑋‘𝑥) ≠ 0 ↔ 𝑥 ∈ 𝑈))
40	36, 39	mpbird 260	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ≠ 0)
41		eldifsn 4751	. . . . . . . 8 ⊢ ((𝑋‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝑋‘𝑥) ∈ ℂ ∧ (𝑋‘𝑥) ≠ 0))
42	35, 40, 41	sylanbrc 595	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
43	42	ralrimiva 3156	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
44	31	ffund 6711	. . . . . . 7 ⊢ (𝜑 → Fun 𝑋)
45	31	fdmd 6717	. . . . . . . 8 ⊢ (𝜑 → dom 𝑋 = (Base‘𝑍))
46	32, 45	sseqtrrid 3977	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ dom 𝑋)
47		funimass4 6946	. . . . . . 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 3973	. . . 4 ⊢ (𝜑 → ran (𝑋 ↾ 𝑈) ⊆ (ℂ ∖ {0}))
51		dchrghm.m	. . . . 5 ⊢ 𝑀 = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
52	51	resmhm2b 18935	. . . 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 20528	. . . 4 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
56	13, 55	syl 18	. . 3 ⊢ (𝜑 → 𝐻 ∈ Grp)
57	51	cnmgpabl 21645	. . . 4 ⊢ 𝑀 ∈ Abel
58		ablgrp 19916	. . . 4 ⊢ (𝑀 ∈ Abel → 𝑀 ∈ Grp)
59	57, 58	ax-mp 5	. . 3 ⊢ 𝑀 ∈ Grp
60		ghmmhmb 19358	. . 3 ⊢ ((𝐻 ∈ Grp ∧ 𝑀 ∈ Grp) → (𝐻 GrpHom 𝑀) = (𝐻 MndHom 𝑀))
61	56, 59, 60	sylancl 598	. 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 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∖ cdif 3899 ⊆ wss 3902 {csn 4587 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 Fun wfun 6531 ⟶wf 6533 ‘cfv 6537 (class class class)co 7416 ℂcc 11125 0cc0 11127 ℕcn 12260 ℕ₀cn0 12531 Basecbs 17305 ↾_s cress 17326 MndHom cmhm 18893 SubMndcsubmnd 18894 Grpcgrp 19061 GrpHom cghm 19344 Abelcabl 19912 mulGrpcmgp 20277 Ringcrg 20376 CRingccrg 20377 Unitcui 20500 ℂ_fldccnfld 21589 ℤ/nℤczn 21719 DChrcdchr 27469

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7739 ax-cnex 11183 ax-resscn 11184 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-mulcom 11191 ax-addass 11192 ax-mulass 11193 ax-distr 11194 ax-i2m1 11195 ax-1ne0 11196 ax-1rid 11197 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200 ax-pre-lttri 11201 ax-pre-lttrn 11202 ax-pre-ltadd 11203 ax-pre-mulgt0 11204 ax-addf 11206 ax-mulf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 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 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-1st 7989 df-2nd 7990 df-tpos 8227 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8458 df-er 8699 df-ec 8701 df-qs 8705 df-map 8831 df-en 8956 df-dom 8957 df-sdom 8958 df-fin 8959 df-sup 9415 df-inf 9416 df-pnf 11272 df-mnf 11273 df-xr 11274 df-ltxr 11275 df-le 11276 df-sub 11470 df-neg 11471 df-div 11899 df-nn 12261 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-n0 12532 df-z 12619 df-dec 12740 df-uz 12891 df-fz 13564 df-struct 17243 df-sets 17260 df-slot 17278 df-ndx 17290 df-base 17306 df-ress 17327 df-plusg 17359 df-mulr 17360 df-starv 17361 df-sca 17362 df-vsca 17363 df-ip 17364 df-tset 17365 df-ple 17366 df-ds 17368 df-unif 17369 df-0g 17530 df-imas 17598 df-qus 17599 df-mgm 18734 df-sgrp 18825 df-mnd 18841 df-mhm 18895 df-submnd 18896 df-grp 19064 df-minusg 19065 df-sbg 19066 df-subg 19250 df-nsg 19251 df-eqg 19252 df-ghm 19345 df-cmn 19913 df-abl 19914 df-mgp 20278 df-rng 20292 df-ur 20325 df-ring 20378 df-cring 20379 df-oppr 20482 df-dvdsr 20502 df-unit 20503 df-invr 20533 df-dvr 20546 df-subrng 20712 df-subrg 20736 df-drng 20896 df-lmod 21050 df-lss 21120 df-lsp 21160 df-sra 21361 df-rgmod 21362 df-lidl 21399 df-rsp 21400 df-2idl 21456 df-cnfld 21590 df-zring 21664 df-zn 21723 df-dchr 27470

This theorem is used by: dchrabs 27497 sum2dchr 27511

W3C validator