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

Metamath Proof Explorer

Theorem dchrelbas

Description: A Dirichlet character is a monoid homomorphism from the multiplicative monoid on Z/nZ to the multiplicative monoid of CC , which is zero off the group of units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrval.g ⊢ G = DChr ⁡ N
dchrval.z ⊢ Z = ℤ/Nℤ
dchrval.b ⊢ B = Base Z
dchrval.u ⊢ U = Unit ⁡ Z
dchrval.n ⊢ φ → N ∈ ℕ
dchrbas.b ⊢ D = Base G
Assertion dchrelbas ⊢ φ → X ∈ D ↔ X ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ B ∖ U × 0 ⊆ X

Proof

Step Hyp Ref Expression
1 dchrval.g ⊢ G = DChr ⁡ N
2 dchrval.z ⊢ Z = ℤ/Nℤ
3 dchrval.b ⊢ B = Base Z
4 dchrval.u ⊢ U = Unit ⁡ Z
5 dchrval.n ⊢ φ → N ∈ ℕ
6 dchrbas.b ⊢ D = Base G
7 1 2 3 4 5 6 dchrbas ⊢ φ → D = x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
8 7 eleq2d ⊢ φ → X ∈ D ↔ X ∈ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
9 sseq2 ⊢ x = X → B ∖ U × 0 ⊆ x ↔ B ∖ U × 0 ⊆ X
10 9 elrab ⊢ X ∈ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x ↔ X ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ B ∖ U × 0 ⊆ X
11 8 10 bitrdi ⊢ φ → X ∈ D ↔ X ∈ mulGrp Z MndHom mulGrp ℂ fld ∧ B ∖ U × 0 ⊆ X