This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑁 ∈ 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 ⊢ ( 𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ )