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

Metamath Proof Explorer

Theorem dchrbas

Description: Base set of the group of Dirichlet characters. (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 dchrbas ⊢ φ → 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 eqidd ⊢ φ → x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x = x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
8 1 2 3 4 5 7 dchrval ⊢ φ → G = Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
9 8 fveq2d ⊢ φ → Base G = Base Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
10 ovex ⊢ mulGrp Z MndHom mulGrp ℂ fld ∈ V
11 10 rabex ⊢ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x ∈ V
12 eqid ⊢ Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x = Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
13 12 grpbase ⊢ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x ∈ V → x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x = Base Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
14 11 13 ax-mp ⊢ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x = Base Base ndx x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x + ndx ∘ f ⁡ × ↾ x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x × x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x
15 9 6 14 3eqtr4g ⊢ φ → D = x ∈ mulGrp Z MndHom mulGrp ℂ fld | B ∖ U × 0 ⊆ x