dchrrcl

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

Step	Hyp	Ref	Expression
1		dchrrcl.g	$⊢ G = DChr (N)$
2		dchrrcl.b	$⊢ D = {Base}_{G}$
3		df-dchr	$⊢ DChr = (n \in ℕ ⟼ ⦋ ℤ / n ℤ / z ⦌ ⦋ \{x \in ({mulGrp}_{z} MndHom {mulGrp}_{ℂ_{fld}}) \| ({Base}_{z} ∖ Unit (z)) \times \{0\} \subseteq x\} / b ⦌ \{⟨{Base}_{ndx}, b⟩, ⟨+_{ndx}, {\circ_{f} \times ↾}_{(b \times b)}⟩\})$
4	3	dmmptss	$⊢ dom DChr \subseteq ℕ$
5		n0i	$⊢ X \in D \to \neg D = \emptyset$
6		ndmfv	$⊢ \neg N \in dom DChr \to DChr (N) = \emptyset$
7	1 6	eqtrid	$⊢ \neg N \in dom DChr \to G = \emptyset$
8		fveq2	$⊢ G = \emptyset \to {Base}_{G} = {Base}_{\emptyset}$
9		base0	$⊢ \emptyset = {Base}_{\emptyset}$
10	8 2 9	3eqtr4g	$⊢ G = \emptyset \to D = \emptyset$
11	7 10	syl	$⊢ \neg N \in dom DChr \to D = \emptyset$
12	5 11	nsyl2	$⊢ X \in D \to N \in dom DChr$
13	4 12	sselid	$⊢ X \in D \to N \in ℕ$

Metamath Proof Explorer