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