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

Metamath Proof Explorer

Theorem dchr1cl

Description: Closure of the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g ⊢ G = DChr ⁡ N
dchrmhm.z ⊢ Z = ℤ/Nℤ
dchrmhm.b ⊢ D = Base G
dchrn0.b ⊢ B = Base Z
dchrn0.u ⊢ U = Unit ⁡ Z
dchr1cl.o ⊢ 1 ˙ = k ∈ B ⟼ if k ∈ U 1 0
dchr1cl.n ⊢ φ → N ∈ ℕ
Assertion dchr1cl ⊢ φ → 1 ˙ ∈ D

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ G = DChr ⁡ N
2 dchrmhm.z ⊢ Z = ℤ/Nℤ
3 dchrmhm.b ⊢ D = Base G
4 dchrn0.b ⊢ B = Base Z
5 dchrn0.u ⊢ U = Unit ⁡ Z
6 dchr1cl.o ⊢ 1 ˙ = k ∈ B ⟼ if k ∈ U 1 0
7 dchr1cl.n ⊢ φ → N ∈ ℕ
8 eqidd ⊢ k = x → 1 = 1
9 eqidd ⊢ k = y → 1 = 1
10 eqidd ⊢ k = x ⋅ Z y → 1 = 1
11 eqidd ⊢ k = 1 Z → 1 = 1
12 1cnd ⊢ φ ∧ k ∈ U → 1 ∈ ℂ
13 1t1e1 ⊢ 1 ⋅ 1 = 1
14 13 eqcomi ⊢ 1 = 1 ⋅ 1
15 14 a1i ⊢ φ ∧ x ∈ U ∧ y ∈ U → 1 = 1 ⋅ 1
16 eqidd ⊢ φ → 1 = 1
17 1 2 4 5 7 3 8 9 10 11 12 15 16 dchrelbasd ⊢ φ → k ∈ B ⟼ if k ∈ U 1 0 ∈ D
18 6 17 eqeltrid ⊢ φ → 1 ˙ ∈ D