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 ∈ 𝐷 )