Theorem dchrzrhcl

Description: A Dirichlet character takes values in the complex numbers. (Contributed by Mario Carneiro, 12-May-2016)

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

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		dchrzrh1.a	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
7		eqid	⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
8	1 2 3 7 5	dchrf	⊢ ( 𝜑 → 𝑋 : ( Base ‘ 𝑍 ) ⟶ ℂ )
9	1 3	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )
10		nnnn0	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
11	5 9 10	3syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12	2 7 4	znzrhfo	⊢ ( 𝑁 ∈ ℕ0 → 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
13		fof	⊢ ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
14	11 12 13	3syl	⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
15	14 6	ffvelcdmd	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐴 ) ∈ ( Base ‘ 𝑍 ) )
16	8 15	ffvelcdmd	⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ )