Theorem dchr1cl

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

	Ref	Expression
Hypotheses	dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
	dchrn0.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrn0.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
	dchr1cl.o	$$⊢\underset{\dot{}}{1}=\left(k\in B⟼if\left(k\in U,1,0\right)\right)$$
	dchr1cl.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	dchr1cl	$$⊢\phi \to \underset{\dot{}}{1}\in D$$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchrmhm.b	$$⊢D={\mathrm{Base}}_G$$
4		dchrn0.b	$$⊢B={\mathrm{Base}}_Z$$
5		dchrn0.u	$$⊢U=\mathrm{Unit}\left(Z\right)$$
6		dchr1cl.o	$$⊢\underset{\dot{}}{1}=\left(k\in B⟼if\left(k\in U,1,0\right)\right)$$
7		dchr1cl.n	$$⊢\phi \to N\in \mathbb{N}$$
8		eqidd	$$⊢k=x\to 1=1$$
9		eqidd	$$⊢k=y\to 1=1$$
10		eqidd	$$⊢k=x{\cdot }_{Z}y\to 1=1$$
11		eqidd	$$⊢k=1_Z\to 1=1$$
12		1cnd	$$⊢\left(\phi \wedge k\in U\right)\to 1\in ℂ$$
13		1t1e1	$$⊢1\cdot 1=1$$
14	13	eqcomi	$$⊢1=1\cdot 1$$
15	14	a1i	$$⊢\left(\phi \wedge \left(x\in U\wedge y\in U\right)\right)\to 1=1\cdot 1$$
16		eqidd	$$⊢\phi \to 1=1$$
17	1 2 4 5 7 3 8 9 10 11 12 15 16	dchrelbasd	$$⊢\phi \to \left(k\in B⟼if\left(k\in U,1,0\right)\right)\in D$$
18	6 17	eqeltrid	$$⊢\phi \to \underset{\dot{}}{1}\in D$$