Metamath Proof Explorer

Theorem dchr1

Description: Value of the principal Dirichlet character. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchr1.g 
|- G = ( DChr ` N )
dchr1.z 
|- Z = ( Z/nZ ` N )
dchr1.o 
|- .1. = ( 0g ` G )
dchr1.u 
|- U = ( Unit ` Z )
dchr1.n 
|- ( ph -> N e. NN )
dchr1.a 
|- ( ph -> A e. U )
Assertion dchr1 
|- ( ph -> ( .1. ` A ) = 1 )

Proof

Step Hyp Ref Expression
1 dchr1.g 
 |-  G = ( DChr ` N )
2 dchr1.z 
 |-  Z = ( Z/nZ ` N )
3 dchr1.o 
 |-  .1. = ( 0g ` G )
4 dchr1.u 
 |-  U = ( Unit ` Z )
5 dchr1.n 
 |-  ( ph -> N e. NN )
6 dchr1.a 
 |-  ( ph -> A e. U )
7 eqid 
 |-  ( Base ` G ) = ( Base ` G )
8 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
9 eqid 
 |-  ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) )
10 1 2 7 8 4 9 5 dchr1cl 
 |-  ( ph -> ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) e. ( Base ` G ) )
11 eleq1w 
 |-  ( k = x -> ( k e. U <-> x e. U ) )
12 11 ifbid 
 |-  ( k = x -> if ( k e. U , 1 , 0 ) = if ( x e. U , 1 , 0 ) )
13 12 cbvmptv 
 |-  ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) = ( x e. ( Base ` Z ) |-> if ( x e. U , 1 , 0 ) )
14 eqid 
 |-  ( +g ` G ) = ( +g ` G )
15 1 2 7 8 4 13 14 10 dchrmulid2 
 |-  ( ph -> ( ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ( +g ` G ) ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) )
16 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
17 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
18 7 14 3 isgrpid2 
 |-  ( G e. Grp -> ( ( ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) e. ( Base ` G ) /\ ( ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ( +g ` G ) ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) <-> .1. = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) )
19 5 16 17 18 4syl 
 |-  ( ph -> ( ( ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) e. ( Base ` G ) /\ ( ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ( +g ` G ) ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) <-> .1. = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) ) )
20 10 15 19 mpbi2and 
 |-  ( ph -> .1. = ( k e. ( Base ` Z ) |-> if ( k e. U , 1 , 0 ) ) )
21 simpr 
 |-  ( ( ph /\ k = A ) -> k = A )
22 6 adantr 
 |-  ( ( ph /\ k = A ) -> A e. U )
23 21 22 eqeltrd 
 |-  ( ( ph /\ k = A ) -> k e. U )
24 23 iftrued 
 |-  ( ( ph /\ k = A ) -> if ( k e. U , 1 , 0 ) = 1 )
25 8 4 unitss 
 |-  U C_ ( Base ` Z )
26 25 6 sselid 
 |-  ( ph -> A e. ( Base ` Z ) )
27 1cnd 
 |-  ( ph -> 1 e. CC )
28 20 24 26 27 fvmptd 
 |-  ( ph -> ( .1. ` A ) = 1 )