Theorem dchrrcl

Description: Reverse closure for a Dirichlet character. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	dchrrcl.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrrcl.b	$$⊢D={\mathrm{Base}}_G$$
Assertion	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		dchrrcl.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrrcl.b	$$⊢D={\mathrm{Base}}_G$$
3		df-dchr	$$⊢\mathrm{DChr}=\left(n\in \mathbb{N}⟼⦋\mathbb{Z}/n\mathbb{Z}/z⦌⦋\left\{x\in \left({\mathrm{mulGrp}}_z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)|\left({\mathrm{Base}}_z\setminus \mathrm{Unit}\left(z\right)\right)\times \left\{0\right\}\subseteq x\right\}/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},{{\circ }_f\times \upharpoonright }_{\left(b\times b\right)}⟩\right\}\right)$$
4	3	dmmptss	$$⊢\mathrm{dom}\mathrm{DChr}\subseteq \mathbb{N}$$
5		n0i	$$⊢X\in D\to \neg D=\varnothing$$
6		ndmfv	$$⊢\neg N\in \mathrm{dom}\mathrm{DChr}\to \mathrm{DChr}\left(N\right)=\varnothing$$
7	1 6	eqtrid	$$⊢\neg N\in \mathrm{dom}\mathrm{DChr}\to G=\varnothing$$
8		fveq2	$$⊢G=\varnothing \to {\mathrm{Base}}_G={\mathrm{Base}}_{\varnothing }$$
9		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
10	8 2 9	3eqtr4g	$$⊢G=\varnothing \to D=\varnothing$$
11	7 10	syl	$$⊢\neg N\in \mathrm{dom}\mathrm{DChr}\to D=\varnothing$$
12	5 11	nsyl2	$$⊢X\in D\to N\in \mathrm{dom}\mathrm{DChr}$$
13	4 12	sselid	$$⊢X\in D\to N\in \mathbb{N}$$