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 25202

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 25187	. . . . 5 ⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld))
5		dchrghm.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝐷)
6	4, 5	sseldi 3750	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)))
7	1, 3	dchrrcl 25186	. . . . . . . . 9 ⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ)
8	5, 7	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
9	8	nnnn0d 11553	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
10	2	zncrng 20108	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → 𝑍 ∈ CRing)
11	9, 10	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ CRing)
12		crngring 18766	. . . . . 6 ⊢ (𝑍 ∈ CRing → 𝑍 ∈ Ring)
13	11, 12	syl 17	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ Ring)
14		dchrghm.u	. . . . . 6 ⊢ 𝑈 = (Unit‘𝑍)
15		eqid 2771	. . . . . 6 ⊢ (mulGrp‘𝑍) = (mulGrp‘𝑍)
16	14, 15	unitsubm 18878	. . . . 5 ⊢ (𝑍 ∈ Ring → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
17	13, 16	syl 17	. . . 4 ⊢ (𝜑 → 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍)))
18		dchrghm.h	. . . . 5 ⊢ 𝐻 = ((mulGrp‘𝑍) ↾_s 𝑈)
19	18	resmhm 17567	. . . 4 ⊢ ((𝑋 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂ_fld)) ∧ 𝑈 ∈ (SubMnd‘(mulGrp‘𝑍))) → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
20	6, 17, 19	syl2anc 573	. . 3 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)))
21		cnring 19983	. . . . 5 ⊢ ℂ_fld ∈ Ring
22		cnfldbas 19965	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
23		cnfld0 19985	. . . . . . 7 ⊢ 0 = (0_g‘ℂ_fld)
24		cndrng 19990	. . . . . . 7 ⊢ ℂ_fld ∈ DivRing
25	22, 23, 24	drngui 18963	. . . . . 6 ⊢ (ℂ ∖ {0}) = (Unit‘ℂ_fld)
26		eqid 2771	. . . . . 6 ⊢ (mulGrp‘ℂ_fld) = (mulGrp‘ℂ_fld)
27	25, 26	unitsubm 18878	. . . . 5 ⊢ (ℂ_fld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)))
28	21, 27	ax-mp 5	. . . 4 ⊢ (ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld))
29		df-ima 5262	. . . . 5 ⊢ (𝑋 “ 𝑈) = ran (𝑋 ↾ 𝑈)
30		eqid 2771	. . . . . . . . . 10 ⊢ (Base‘𝑍) = (Base‘𝑍)
31	1, 2, 3, 30, 5	dchrf 25188	. . . . . . . . 9 ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℂ)
32	30, 14	unitss 18868	. . . . . . . . . 10 ⊢ 𝑈 ⊆ (Base‘𝑍)
33	32	sseli 3748	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝑈 → 𝑥 ∈ (Base‘𝑍))
34		ffvelrn 6500	. . . . . . . . 9 ⊢ ((𝑋:(Base‘𝑍)⟶ℂ ∧ 𝑥 ∈ (Base‘𝑍)) → (𝑋‘𝑥) ∈ ℂ)
35	31, 33, 34	syl2an 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ∈ ℂ)
36		simpr 471	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ 𝑈)
37	5	adantr 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑋 ∈ 𝐷)
38	33	adantl 467	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → 𝑥 ∈ (Base‘𝑍))
39	1, 2, 3, 30, 14, 37, 38	dchrn0 25196	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → ((𝑋‘𝑥) ≠ 0 ↔ 𝑥 ∈ 𝑈))
40	36, 39	mpbird 247	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ≠ 0)
41		eldifsn 4453	. . . . . . . 8 ⊢ ((𝑋‘𝑥) ∈ (ℂ ∖ {0}) ↔ ((𝑋‘𝑥) ∈ ℂ ∧ (𝑋‘𝑥) ≠ 0))
42	35, 40, 41	sylanbrc 572	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑈) → (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
43	42	ralrimiva 3115	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0}))
44		ffun 6188	. . . . . . . 8 ⊢ (𝑋:(Base‘𝑍)⟶ℂ → Fun 𝑋)
45	31, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → Fun 𝑋)
46		fdm 6191	. . . . . . . . 9 ⊢ (𝑋:(Base‘𝑍)⟶ℂ → dom 𝑋 = (Base‘𝑍))
47	31, 46	syl 17	. . . . . . . 8 ⊢ (𝜑 → dom 𝑋 = (Base‘𝑍))
48	32, 47	syl5sseqr 3803	. . . . . . 7 ⊢ (𝜑 → 𝑈 ⊆ dom 𝑋)
49		funimass4 6389	. . . . . . 7 ⊢ ((Fun 𝑋 ∧ 𝑈 ⊆ dom 𝑋) → ((𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}) ↔ ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0})))
50	45, 48, 49	syl2anc 573	. . . . . 6 ⊢ (𝜑 → ((𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}) ↔ ∀𝑥 ∈ 𝑈 (𝑋‘𝑥) ∈ (ℂ ∖ {0})))
51	43, 50	mpbird 247	. . . . 5 ⊢ (𝜑 → (𝑋 “ 𝑈) ⊆ (ℂ ∖ {0}))
52	29, 51	syl5eqssr 3799	. . . 4 ⊢ (𝜑 → ran (𝑋 ↾ 𝑈) ⊆ (ℂ ∖ {0}))
53		dchrghm.m	. . . . 5 ⊢ 𝑀 = ((mulGrp‘ℂ_fld) ↾_s (ℂ ∖ {0}))
54	53	resmhm2b 17569	. . . 4 ⊢ (((ℂ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℂ_fld)) ∧ ran (𝑋 ↾ 𝑈) ⊆ (ℂ ∖ {0})) → ((𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)) ↔ (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀)))
55	28, 52, 54	sylancr 575	. . 3 ⊢ (𝜑 → ((𝑋 ↾ 𝑈) ∈ (𝐻 MndHom (mulGrp‘ℂ_fld)) ↔ (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀)))
56	20, 55	mpbid 222	. 2 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 MndHom 𝑀))
57	14, 18	unitgrp 18875	. . . 4 ⊢ (𝑍 ∈ Ring → 𝐻 ∈ Grp)
58	13, 57	syl 17	. . 3 ⊢ (𝜑 → 𝐻 ∈ Grp)
59	53	cnmgpabl 20022	. . . 4 ⊢ 𝑀 ∈ Abel
60		ablgrp 18405	. . . 4 ⊢ (𝑀 ∈ Abel → 𝑀 ∈ Grp)
61	59, 60	ax-mp 5	. . 3 ⊢ 𝑀 ∈ Grp
62		ghmmhmb 17879	. . 3 ⊢ ((𝐻 ∈ Grp ∧ 𝑀 ∈ Grp) → (𝐻 GrpHom 𝑀) = (𝐻 MndHom 𝑀))
63	58, 61, 62	sylancl 574	. 2 ⊢ (𝜑 → (𝐻 GrpHom 𝑀) = (𝐻 MndHom 𝑀))
64	56, 63	eleqtrrd 2853	1 ⊢ (𝜑 → (𝑋 ↾ 𝑈) ∈ (𝐻 GrpHom 𝑀))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ≠ wne 2943 ∀wral 3061 ∖ cdif 3720 ⊆ wss 3723 {csn 4316 dom cdm 5249 ran crn 5250 ↾ cres 5251 “ cima 5252 Fun wfun 6025 ⟶wf 6027 ‘cfv 6031 (class class class)co 6793 ℂcc 10136 0cc0 10138 ℕcn 11222 ℕ₀cn0 11494 Basecbs 16064 ↾_s cress 16065 MndHom cmhm 17541 SubMndcsubmnd 17542 Grpcgrp 17630 GrpHom cghm 17865 Abelcabl 18401 mulGrpcmgp 18697 Ringcrg 18755 CRingccrg 18756 Unitcui 18847 ℂ_fldccnfld 19961 ℤ/nℤczn 20066 DChrcdchr 25178

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-rep 4904 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 ax-cnex 10194 ax-resscn 10195 ax-1cn 10196 ax-icn 10197 ax-addcl 10198 ax-addrcl 10199 ax-mulcl 10200 ax-mulrcl 10201 ax-mulcom 10202 ax-addass 10203 ax-mulass 10204 ax-distr 10205 ax-i2m1 10206 ax-1ne0 10207 ax-1rid 10208 ax-rnegex 10209 ax-rrecex 10210 ax-cnre 10211 ax-pre-lttri 10212 ax-pre-lttrn 10213 ax-pre-ltadd 10214 ax-pre-mulgt0 10215 ax-addf 10217 ax-mulf 10218

This theorem depends on definitions: df-bi 197 df-an 383 df-or 837 df-3or 1072 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-nel 3047 df-ral 3066 df-rex 3067 df-reu 3068 df-rmo 3069 df-rab 3070 df-v 3353 df-sbc 3588 df-csb 3683 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-pss 3739 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-tp 4321 df-op 4323 df-uni 4575 df-int 4612 df-iun 4656 df-br 4787 df-opab 4847 df-mpt 4864 df-tr 4887 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-riota 6754 df-ov 6796 df-oprab 6797 df-mpt2 6798 df-om 7213 df-1st 7315 df-2nd 7316 df-tpos 7504 df-wrecs 7559 df-recs 7621 df-rdg 7659 df-1o 7713 df-oadd 7717 df-er 7896 df-ec 7898 df-qs 7902 df-map 8011 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8504 df-inf 8505 df-pnf 10278 df-mnf 10279 df-xr 10280 df-ltxr 10281 df-le 10282 df-sub 10470 df-neg 10471 df-div 10887 df-nn 11223 df-2 11281 df-3 11282 df-4 11283 df-5 11284 df-6 11285 df-7 11286 df-8 11287 df-9 11288 df-n0 11495 df-z 11580 df-dec 11696 df-uz 11889 df-fz 12534 df-struct 16066 df-ndx 16067 df-slot 16068 df-base 16070 df-sets 16071 df-ress 16072 df-plusg 16162 df-mulr 16163 df-starv 16164 df-sca 16165 df-vsca 16166 df-ip 16167 df-tset 16168 df-ple 16169 df-ds 16172 df-unif 16173 df-0g 16310 df-imas 16376 df-qus 16377 df-mgm 17450 df-sgrp 17492 df-mnd 17503 df-mhm 17543 df-submnd 17544 df-grp 17633 df-minusg 17634 df-sbg 17635 df-subg 17799 df-nsg 17800 df-eqg 17801 df-ghm 17866 df-cmn 18402 df-abl 18403 df-mgp 18698 df-ur 18710 df-ring 18757 df-cring 18758 df-oppr 18831 df-dvdsr 18849 df-unit 18850 df-invr 18880 df-dvr 18891 df-drng 18959 df-subrg 18988 df-lmod 19075 df-lss 19143 df-lsp 19185 df-sra 19387 df-rgmod 19388 df-lidl 19389 df-rsp 19390 df-2idl 19447 df-cnfld 19962 df-zring 20034 df-zn 20070 df-dchr 25179

This theorem is referenced by: dchrabs 25206 sum2dchr 25220

W3C validator