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 = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrelbas4.l 
|- L = ( ZRHom ` Z )
dchrzrh1.x 
|- ( ph -> X e. D )
Assertion dchrzrh1 
|- ( ph -> ( X ` ( L ` 1 ) ) = 1 )

Proof

Step Hyp Ref Expression
1 dchrmhm.g 
 |-  G = ( DChr ` N )
2 dchrmhm.z 
 |-  Z = ( Z/nZ ` N )
3 dchrmhm.b 
 |-  D = ( Base ` G )
4 dchrelbas4.l 
 |-  L = ( ZRHom ` Z )
5 dchrzrh1.x 
 |-  ( ph -> X e. D )
6 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
7 5 6 syl 
 |-  ( ph -> N e. NN )
8 7 nnnn0d 
 |-  ( ph -> N e. NN0 )
9 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
10 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
11 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
12 4 11 zrh1 
 |-  ( Z e. Ring -> ( L ` 1 ) = ( 1r ` Z ) )
13 8 9 10 12 4syl 
 |-  ( ph -> ( L ` 1 ) = ( 1r ` Z ) )
14 13 fveq2d 
 |-  ( ph -> ( X ` ( L ` 1 ) ) = ( X ` ( 1r ` Z ) ) )
15 1 2 3 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
16 15 5 sselid 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
17 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
18 17 11 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
19 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
20 cnfld1 
 |-  1 = ( 1r ` CCfld )
21 19 20 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
22 18 21 mhm0 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 )
23 16 22 syl 
 |-  ( ph -> ( X ` ( 1r ` Z ) ) = 1 )
24 14 23 eqtrd 
 |-  ( ph -> ( X ` ( L ` 1 ) ) = 1 )