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 ⊢ G = DChr ⁡ N
dchrmhm.z ⊢ Z = ℤ/Nℤ
dchrmhm.b ⊢ D = Base G
dchrelbas4.l ⊢ L = ℤRHom ⁡ Z
dchrzrh1.x ⊢ φ → X ∈ D
dchrzrh1.a ⊢ φ → A ∈ ℤ
Assertion dchrzrhcl ⊢ φ → X ⁡ L ⁡ A ∈ ℂ

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ G = DChr ⁡ N
2 dchrmhm.z ⊢ Z = ℤ/Nℤ
3 dchrmhm.b ⊢ D = Base G
4 dchrelbas4.l ⊢ L = ℤRHom ⁡ Z
5 dchrzrh1.x ⊢ φ → X ∈ D
6 dchrzrh1.a ⊢ φ → A ∈ ℤ
7 eqid ⊢ Base Z = Base Z
8 1 2 3 7 5 dchrf ⊢ φ → X : Base Z ⟶ ℂ
9 1 3 dchrrcl ⊢ X ∈ D → N ∈ ℕ
10 nnnn0 ⊢ N ∈ ℕ → N ∈ ℕ 0
11 5 9 10 3syl ⊢ φ → N ∈ ℕ 0
12 2 7 4 znzrhfo ⊢ N ∈ ℕ 0 → L : ℤ ⟶ onto Base Z
13 fof ⊢ L : ℤ ⟶ onto Base Z → L : ℤ ⟶ Base Z
14 11 12 13 3syl ⊢ φ → L : ℤ ⟶ Base Z
15 14 6 ffvelcdmd ⊢ φ → L ⁡ A ∈ Base Z
16 8 15 ffvelcdmd ⊢ φ → X ⁡ L ⁡ A ∈ ℂ