Theorem dchrrcl

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

	Ref	Expression
Hypotheses	dchrrcl.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchrrcl.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion	dchrrcl	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		dchrrcl.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchrrcl.b	⊢ 𝐷 = ( Base ‘ 𝐺 )
3		df-dchr	⊢ DChr = ( 𝑛 ∈ ℕ ↦ ⦋ ( ℤ/nℤ ‘ 𝑛 ) / 𝑧 ⦌ ⦋ { 𝑥 ∈ ( ( mulGrp ‘ 𝑧 ) MndHom ( mulGrp ‘ ℂfld ) ) ∣ ( ( ( Base ‘ 𝑧 ) ∖ ( Unit ‘ 𝑧 ) ) × { 0 } ) ⊆ 𝑥 } / 𝑏 ⦌ { ⟨ ( Base ‘ ndx ) , 𝑏 ⟩ , ⟨ ( +g ‘ ndx ) , ( ∘f · ↾ ( 𝑏 × 𝑏 ) ) ⟩ } )
4	3	dmmptss	⊢ dom DChr ⊆ ℕ
5		n0i	⊢ ( 𝑋 ∈ 𝐷 → ¬ 𝐷 = ∅ )
6		ndmfv	⊢ ( ¬ 𝑁 ∈ dom DChr → ( DChr ‘ 𝑁 ) = ∅ )
7	1 6	syl5eq	⊢ ( ¬ 𝑁 ∈ dom DChr → 𝐺 = ∅ )
8		fveq2	⊢ ( 𝐺 = ∅ → ( Base ‘ 𝐺 ) = ( Base ‘ ∅ ) )
9		base0	⊢ ∅ = ( Base ‘ ∅ )
10	8 2 9	3eqtr4g	⊢ ( 𝐺 = ∅ → 𝐷 = ∅ )
11	7 10	syl	⊢ ( ¬ 𝑁 ∈ dom DChr → 𝐷 = ∅ )
12	5 11	nsyl2	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ dom DChr )
13	4 12	sselid	⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )