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

Metamath Proof Explorer

Theorem dchrmhm

Description: A Dirichlet character is a monoid homomorphism. (Contributed by Mario Carneiro, 19-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
Assertion dchrmhm 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrmhm.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3 dchrmhm.b ⊢ 𝐷 = ( Base ‘ 𝐺 )
4 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
5 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
6 1 3 dchrrcl ⊢ ( 𝑥 ∈ 𝐷 → 𝑁 ∈ ℕ )
7 1 2 4 5 6 3 dchrelbas ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) ) )
8 7 ibi ⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) ∧ ( ( ( Base ‘ 𝑍 ) ∖ ( Unit ‘ 𝑍 ) ) × { 0 } ) ⊆ 𝑥 ) )
9 8 simpld ⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
10 9 ssriv ⊢ 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )