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

Metamath Proof Explorer

Theorem dchr1cl

Description: Closure of 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 ) )
dchr1cl.n 
|- ( ph -> N e. NN )
Assertion dchr1cl 
|- ( ph -> .1. e. D )

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 dchr1cl.n 
 |-  ( ph -> N e. NN )
8 eqidd 
 |-  ( k = x -> 1 = 1 )
9 eqidd 
 |-  ( k = y -> 1 = 1 )
10 eqidd 
 |-  ( k = ( x ( .r ` Z ) y ) -> 1 = 1 )
11 eqidd 
 |-  ( k = ( 1r ` Z ) -> 1 = 1 )
12 1cnd 
 |-  ( ( ph /\ k e. U ) -> 1 e. CC )
13 1t1e1 
 |-  ( 1 x. 1 ) = 1
14 13 eqcomi 
 |-  1 = ( 1 x. 1 )
15 14 a1i 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> 1 = ( 1 x. 1 ) )
16 eqidd 
 |-  ( ph -> 1 = 1 )
17 1 2 4 5 7 3 8 9 10 11 12 15 16 dchrelbasd 
 |-  ( ph -> ( k e. B |-> if ( k e. U , 1 , 0 ) ) e. D )
18 6 17 eqeltrid 
 |-  ( ph -> .1. e. D )