This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 𝐴 ) ) ∈ ℂ )