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

Metamath Proof Explorer

Theorem dchrmullid

Description: Left identity for the principal Dirichlet character. (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g 
|- G = ( DChr ` N )
dchrmhm.z 
|- Z = ( Z/nZ ` N )
dchrmhm.b 
|- D = ( Base ` G )
dchrn0.b 
|- B = ( Base ` Z )
dchrn0.u 
|- U = ( Unit ` Z )
dchr1cl.o 
|- .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )
dchrmullid.t 
|- .x. = ( +g ` G )
dchrmullid.x 
|- ( ph -> X e. D )
Assertion dchrmullid 
|- ( ph -> ( .1. .x. X ) = X )

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 dchrn0.b 
 |-  B = ( Base ` Z )
5 dchrn0.u 
 |-  U = ( Unit ` Z )
6 dchr1cl.o 
 |-  .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) )
7 dchrmullid.t 
 |-  .x. = ( +g ` G )
8 dchrmullid.x 
 |-  ( ph -> X e. D )
9 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
10 8 9 syl 
 |-  ( ph -> N e. NN )
11 1 2 3 4 5 6 10 dchr1cl 
 |-  ( ph -> .1. e. D )
12 1 2 3 7 11 8 dchrmul 
 |-  ( ph -> ( .1. .x. X ) = ( .1. oF x. X ) )
13 oveq1 
 |-  ( 1 = if ( k e. U , 1 , 0 ) -> ( 1 x. ( X ` k ) ) = ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) )
14 13 eqeq1d 
 |-  ( 1 = if ( k e. U , 1 , 0 ) -> ( ( 1 x. ( X ` k ) ) = ( X ` k ) <-> ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) = ( X ` k ) ) )
15 oveq1 
 |-  ( 0 = if ( k e. U , 1 , 0 ) -> ( 0 x. ( X ` k ) ) = ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) )
16 15 eqeq1d 
 |-  ( 0 = if ( k e. U , 1 , 0 ) -> ( ( 0 x. ( X ` k ) ) = ( X ` k ) <-> ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) = ( X ` k ) ) )
17 1 2 3 4 8 dchrf 
 |-  ( ph -> X : B --> CC )
18 17 ffvelcdmda 
 |-  ( ( ph /\ k e. B ) -> ( X ` k ) e. CC )
19 18 adantr 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> ( X ` k ) e. CC )
20 19 mullidd 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> ( 1 x. ( X ` k ) ) = ( X ` k ) )
21 0cn 
 |-  0 e. CC
22 21 mul02i 
 |-  ( 0 x. 0 ) = 0
23 1 2 4 5 10 3 dchrelbas2 
 |-  ( ph -> ( X e. D <-> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. k e. B ( ( X ` k ) =/= 0 -> k e. U ) ) ) )
24 8 23 mpbid 
 |-  ( ph -> ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ A. k e. B ( ( X ` k ) =/= 0 -> k e. U ) ) )
25 24 simprd 
 |-  ( ph -> A. k e. B ( ( X ` k ) =/= 0 -> k e. U ) )
26 25 r19.21bi 
 |-  ( ( ph /\ k e. B ) -> ( ( X ` k ) =/= 0 -> k e. U ) )
27 26 necon1bd 
 |-  ( ( ph /\ k e. B ) -> ( -. k e. U -> ( X ` k ) = 0 ) )
28 27 imp 
 |-  ( ( ( ph /\ k e. B ) /\ -. k e. U ) -> ( X ` k ) = 0 )
29 28 oveq2d 
 |-  ( ( ( ph /\ k e. B ) /\ -. k e. U ) -> ( 0 x. ( X ` k ) ) = ( 0 x. 0 ) )
30 22 29 28 3eqtr4a 
 |-  ( ( ( ph /\ k e. B ) /\ -. k e. U ) -> ( 0 x. ( X ` k ) ) = ( X ` k ) )
31 14 16 20 30 ifbothda 
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) = ( X ` k ) )
32 31 mpteq2dva 
 |-  ( ph -> ( k e. B |-> ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) ) = ( k e. B |-> ( X ` k ) ) )
33 4 fvexi 
 |-  B e. _V
34 33 a1i 
 |-  ( ph -> B e. _V )
35 ax-1cn 
 |-  1 e. CC
36 35 21 ifcli 
 |-  if ( k e. U , 1 , 0 ) e. CC
37 36 a1i 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , 1 , 0 ) e. CC )
38 6 a1i 
 |-  ( ph -> .1. = ( k e. B |-> if ( k e. U , 1 , 0 ) ) )
39 17 feqmptd 
 |-  ( ph -> X = ( k e. B |-> ( X ` k ) ) )
40 34 37 18 38 39 offval2 
 |-  ( ph -> ( .1. oF x. X ) = ( k e. B |-> ( if ( k e. U , 1 , 0 ) x. ( X ` k ) ) ) )
41 32 40 39 3eqtr4d 
 |-  ( ph -> ( .1. oF x. X ) = X )
42 12 41 eqtrd 
 |-  ( ph -> ( .1. .x. X ) = X )