Theorem dchrzrh1

Description: Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016)

	Ref	Expression
Hypotheses	dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
	dchrelbas4.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	dchrzrh1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
Assertion	dchrzrh1	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrmhm.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchrmhm.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
4		dchrelbas4.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
5		dchrzrh1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
7	5 6	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8	7	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
9	2	zncrng	⊢ ( 𝑁 ∈ ℕ0 → 𝑍 ∈ CRing )
10		crngring	⊢ ( 𝑍 ∈ CRing → 𝑍 ∈ Ring )
11		eqid	⊢ ( 1r ‘ 𝑍 ) = ( 1r ‘ 𝑍 )
12	4 11	zrh1	⊢ ( 𝑍 ∈ Ring → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
13	8 9 10 12	4syl	⊢ ( 𝜑 → ( 𝐿 ‘ 1 ) = ( 1r ‘ 𝑍 ) )
14	13	fveq2d	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) )
15	1 2 3	dchrmhm	⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
16	15 5	sseldi	⊢ ( 𝜑 → 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
17		eqid	⊢ ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
18	17 11	ringidval	⊢ ( 1r ‘ 𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
19		eqid	⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
20		cnfld1	⊢ 1 = ( 1r ‘ ℂfld )
21	19 20	ringidval	⊢ 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
22	18 21	mhm0	⊢ ( 𝑋 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
23	16 22	syl	⊢ ( 𝜑 → ( 𝑋 ‘ ( 1r ‘ 𝑍 ) ) = 1 )
24	14 23	eqtrd	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )