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

Metamath Proof Explorer

Theorem dchrzrh1

Description: Value of a Dirichlet character at one. (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses dchrmhm.g ⊢ G = DChr ⁡ N
dchrmhm.z ⊢ Z = ℤ/Nℤ
dchrmhm.b ⊢ D = Base G
dchrelbas4.l ⊢ L = ℤRHom ⁡ Z
dchrzrh1.x ⊢ φ → X ∈ D
Assertion dchrzrh1 ⊢ φ → X ⁡ L ⁡ 1 = 1

Proof

Step Hyp Ref Expression
1 dchrmhm.g ⊢ G = DChr ⁡ N
2 dchrmhm.z ⊢ Z = ℤ/Nℤ
3 dchrmhm.b ⊢ D = Base G
4 dchrelbas4.l ⊢ L = ℤRHom ⁡ Z
5 dchrzrh1.x ⊢ φ → X ∈ D
6 1 3 dchrrcl ⊢ X ∈ D → N ∈ ℕ
7 5 6 syl ⊢ φ → N ∈ ℕ
8 7 nnnn0d ⊢ φ → N ∈ ℕ 0
9 2 zncrng ⊢ N ∈ ℕ 0 → Z ∈ CRing
10 crngring ⊢ Z ∈ CRing → Z ∈ Ring
11 eqid ⊢ 1 Z = 1 Z
12 4 11 zrh1 ⊢ Z ∈ Ring → L ⁡ 1 = 1 Z
13 8 9 10 12 4syl ⊢ φ → L ⁡ 1 = 1 Z
14 13 fveq2d ⊢ φ → X ⁡ L ⁡ 1 = X ⁡ 1 Z
15 1 2 3 dchrmhm ⊢ D ⊆ mulGrp Z MndHom mulGrp ℂ fld
16 15 5 sselid ⊢ φ → X ∈ mulGrp Z MndHom mulGrp ℂ fld
17 eqid ⊢ mulGrp Z = mulGrp Z
18 17 11 ringidval ⊢ 1 Z = 0 mulGrp Z
19 eqid ⊢ mulGrp ℂ fld = mulGrp ℂ fld
20 cnfld1 ⊢ 1 = 1 ℂ fld
21 19 20 ringidval ⊢ 1 = 0 mulGrp ℂ fld
22 18 21 mhm0 ⊢ X ∈ mulGrp Z MndHom mulGrp ℂ fld → X ⁡ 1 Z = 1
23 16 22 syl ⊢ φ → X ⁡ 1 Z = 1
24 14 23 eqtrd ⊢ φ → X ⁡ L ⁡ 1 = 1