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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrn0.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrn0.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
dchr1cl.o ⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
dchr1cl.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion dchr1cl ( 𝜑 → 1 ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 dchrn0.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchrn0.u ⊢ 𝑈 = ( Unit ‘ 𝑍 )
6 dchr1cl.o ⊢ 1 = ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) )
7 dchr1cl.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
8 eqidd ⊢ ( 𝑘 = 𝑥 → 1 = 1 )
9 eqidd ⊢ ( 𝑘 = 𝑦 → 1 = 1 )
10 eqidd ⊢ ( 𝑘 = ( 𝑥 ( .r ‘ 𝑍 ) 𝑦 ) → 1 = 1 )
11 eqidd ⊢ ( 𝑘 = ( 1r ‘ 𝑍 ) → 1 = 1 )
12 1cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑈 ) → 1 ∈ ℂ )
13 1t1e1 ⊢ ( 1 · 1 ) = 1
14 13 eqcomi ⊢ 1 = ( 1 · 1 )
15 14 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 1 = ( 1 · 1 ) )
16 eqidd ⊢ ( 𝜑 → 1 = 1 )
17 1 2 4 5 7 3 8 9 10 11 12 15 16 dchrelbasd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐵 ↦ if ( 𝑘 ∈ 𝑈 , 1 , 0 ) ) ∈ 𝐷 )
18 6 17 eqeltrid ⊢ ( 𝜑 → 1 ∈ 𝐷 )