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 ⊢ G = DChr ⁡ N
dchrmhm.z ⊢ Z = ℤ/Nℤ
dchrmhm.b ⊢ D = Base G
Assertion dchrmhm ⊢ D ⊆ mulGrp Z MndHom mulGrp ℂ fld

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ G = DChr ⁡ N
2 dchrmhm.z ⊢ Z = ℤ/Nℤ
3 dchrmhm.b ⊢ D = Base G
4 eqid ⊢ Base Z = Base Z
5 eqid ⊢ Unit ⁡ Z = Unit ⁡ Z
6 1 3 dchrrcl ⊢ x ∈ D → N ∈ ℕ
7 1 2 4 5 6 3 dchrelbas ⊢ x ∈ D → x ∈ D ↔ x ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ Base Z ∖ Unit ⁡ Z × 0 ⊆ x
8 7 ibi ⊢ x ∈ D → x ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ Base Z ∖ Unit ⁡ Z × 0 ⊆ x
9 8 simpld ⊢ x ∈ D → x ∈ mulGrp Z MndHom mulGrp ℂ fld
10 9 ssriv ⊢ D ⊆ mulGrp Z MndHom mulGrp ℂ fld