Theorem dchrn0

Description: A Dirichlet character is nonzero on the units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrn0.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchrn0.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
	dchrn0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrn0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion	dchrn0	⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrn0.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		dchrn0.u	⊢ 𝑈 = ( Unit ‘ 𝑍 )
6		dchrn0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
7		dchrn0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
8		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑋 ‘ 𝑥 ) = ( 𝑋 ‘ 𝐴 ) )
9	8	neeq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑋 ‘ 𝑥 ) ≠ 0 ↔ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) )
10		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) )
11	9 10	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ↔ ( ( 𝑋 ‘ 𝐴 ) ≠ 0 → 𝐴 ∈ 𝑈 ) ) )
12	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
13	6 12	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
14	1 2 4 5 13 3	dchrelbas2	⊢ ( 𝜑 → ( 𝑋 ∈ 𝐷 ↔ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) ) )
15	6 14	mpbid	⊢ ( 𝜑 → ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) ) )
16	15	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( ( 𝑋 ‘ 𝑥 ) ≠ 0 → 𝑥 ∈ 𝑈 ) )
17	11 16 7	rspcdva	⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 → 𝐴 ∈ 𝑈 ) )
18	17	imp	⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ 𝑈 )
19		ax-1ne0	⊢ 1 ≠ 0
20	19	a1i	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 1 ≠ 0 )
21	13	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
22	2	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
23		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
24	21 22 23	3syl	⊢ ( 𝜑 → 𝑍 ∈ Ring )
25		eqid	⊢ ( invr ‘ 𝑍 ) = ( invr ‘ 𝑍 )
26		eqid	⊢ ( .r ‘ 𝑍 ) = ( .r ‘ 𝑍 )
27		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
28	5 25 26 27	unitrinv	⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) = ( 1r ‘ 𝑍 ) )
29	24 28	sylan	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) = ( 1r ‘ 𝑍 ) )
30	29	fveq2d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
31	15	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
32	31	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
33	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ 𝐵 )
34	5 25 4	ringinvcl	⊢ ( ( 𝑍 ∈ Ring ∧ 𝐴 ∈ 𝑈 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ∈ 𝐵 )
35	24 34	sylan	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ∈ 𝐵 )
36		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
37	36 4	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑍 ) )
38	36 26	mgpplusg	⊢ ( .r ‘ 𝑍 ) = ( +g ‘ ( mulGrp ‘ 𝑍 ) )
39		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
40		cnfldmul	⊢ · = ( .r ‘ ℂfld )
41	39 40	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ ℂfld ) )
42	37 38 41	mhmlin	⊢ ( ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ 𝐴 ∈ 𝐵 ∧ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ∈ 𝐵 ) → ( 𝑋 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) )
43	32 33 35 42	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ‘ ( 𝐴 ( .r ‘ 𝑍 ) ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) )
44	36 27	ringidval	⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
45		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
46	39 45	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
47	44 46	mhm0	⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
48	32 47	syl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
49	30 43 48	3eqtr3d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = 1 )
50		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
51	39 50	mgpbas	⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
52	37 51	mhmf	⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → 𝑋 : 𝐵 ⟶ ℂ )
53	32 52	syl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → 𝑋 : 𝐵 ⟶ ℂ )
54	53 35	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ∈ ℂ )
55	54	mul02d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 0 · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = 0 )
56	20 49 55	3netr4d	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) ≠ ( 0 · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) )
57		oveq1	⊢ ( ( 𝑋 ‘ 𝐴 ) = 0 → ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) = ( 0 · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) )
58	57	necon3i	⊢ ( ( ( 𝑋 ‘ 𝐴 ) · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) ≠ ( 0 · ( 𝑋 ‘ ( ( invr ‘ 𝑍 ) ‘ 𝐴 ) ) ) → ( 𝑋 ‘ 𝐴 ) ≠ 0 )
59	56 58	syl	⊢ ( ( 𝜑 ∧ 𝐴 ∈ 𝑈 ) → ( 𝑋 ‘ 𝐴 ) ≠ 0 )
60	18 59	impbida	⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ 𝑈 ) )