Metamath Proof Explorer

Theorem dchrinvcl

Description: Closure of the group inverse operation on Dirichlet characters. (Contributed by Mario Carneiro, 19-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 ) )
dchrmulid2.t 
|- .x. = ( +g ` G )
dchrmulid2.x 
|- ( ph -> X e. D )
dchrinvcl.n 
|- K = ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) )
Assertion dchrinvcl 
|- ( ph -> ( K e. D /\ ( K .x. X ) = .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 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 dchrmulid2.t 
 |-  .x. = ( +g ` G )
8 dchrmulid2.x 
 |-  ( ph -> X e. D )
9 dchrinvcl.n 
 |-  K = ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) )
10 1 3 dchrrcl 
 |-  ( X e. D -> N e. NN )
11 8 10 syl 
 |-  ( ph -> N e. NN )
12 fveq2 
 |-  ( k = x -> ( X ` k ) = ( X ` x ) )
13 12 oveq2d 
 |-  ( k = x -> ( 1 / ( X ` k ) ) = ( 1 / ( X ` x ) ) )
14 fveq2 
 |-  ( k = y -> ( X ` k ) = ( X ` y ) )
15 14 oveq2d 
 |-  ( k = y -> ( 1 / ( X ` k ) ) = ( 1 / ( X ` y ) ) )
16 fveq2 
 |-  ( k = ( x ( .r ` Z ) y ) -> ( X ` k ) = ( X ` ( x ( .r ` Z ) y ) ) )
17 16 oveq2d 
 |-  ( k = ( x ( .r ` Z ) y ) -> ( 1 / ( X ` k ) ) = ( 1 / ( X ` ( x ( .r ` Z ) y ) ) ) )
18 fveq2 
 |-  ( k = ( 1r ` Z ) -> ( X ` k ) = ( X ` ( 1r ` Z ) ) )
19 18 oveq2d 
 |-  ( k = ( 1r ` Z ) -> ( 1 / ( X ` k ) ) = ( 1 / ( X ` ( 1r ` Z ) ) ) )
20 1 2 3 4 8 dchrf 
 |-  ( ph -> X : B --> CC )
21 4 5 unitss 
 |-  U C_ B
22 21 sseli 
 |-  ( k e. U -> k e. B )
23 ffvelrn 
 |-  ( ( X : B --> CC /\ k e. B ) -> ( X ` k ) e. CC )
24 20 22 23 syl2an 
 |-  ( ( ph /\ k e. U ) -> ( X ` k ) e. CC )
25 simpr 
 |-  ( ( ph /\ k e. U ) -> k e. U )
26 8 adantr 
 |-  ( ( ph /\ k e. U ) -> X e. D )
27 22 adantl 
 |-  ( ( ph /\ k e. U ) -> k e. B )
28 1 2 3 4 5 26 27 dchrn0 
 |-  ( ( ph /\ k e. U ) -> ( ( X ` k ) =/= 0 <-> k e. U ) )
29 25 28 mpbird 
 |-  ( ( ph /\ k e. U ) -> ( X ` k ) =/= 0 )
30 24 29 reccld 
 |-  ( ( ph /\ k e. U ) -> ( 1 / ( X ` k ) ) e. CC )
31 1t1e1 
 |-  ( 1 x. 1 ) = 1
32 31 eqcomi 
 |-  1 = ( 1 x. 1 )
33 32 a1i 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> 1 = ( 1 x. 1 ) )
34 1 2 3 dchrmhm 
 |-  D C_ ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) )
35 8 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> X e. D )
36 34 35 sseldi 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
37 simprl 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. U )
38 21 37 sseldi 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. B )
39 simprr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. U )
40 21 39 sseldi 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. B )
41 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
42 41 4 mgpbas 
 |-  B = ( Base ` ( mulGrp ` Z ) )
43 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
44 41 43 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
45 eqid 
 |-  ( mulGrp ` CCfld ) = ( mulGrp ` CCfld )
46 cnfldmul 
 |-  x. = ( .r ` CCfld )
47 45 46 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` CCfld ) )
48 42 44 47 mhmlin 
 |-  ( ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) /\ x e. B /\ y e. B ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
49 36 38 40 48 syl3anc 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
50 33 49 oveq12d 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( 1 / ( X ` ( x ( .r ` Z ) y ) ) ) = ( ( 1 x. 1 ) / ( ( X ` x ) x. ( X ` y ) ) ) )
51 1cnd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> 1 e. CC )
52 20 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> X : B --> CC )
53 52 38 ffvelrnd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` x ) e. CC )
54 52 40 ffvelrnd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` y ) e. CC )
55 1 2 3 4 5 35 38 dchrn0 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( X ` x ) =/= 0 <-> x e. U ) )
56 37 55 mpbird 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` x ) =/= 0 )
57 1 2 3 4 5 35 40 dchrn0 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( X ` y ) =/= 0 <-> y e. U ) )
58 39 57 mpbird 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` y ) =/= 0 )
59 51 53 51 54 56 58 divmuldivd 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( 1 / ( X ` x ) ) x. ( 1 / ( X ` y ) ) ) = ( ( 1 x. 1 ) / ( ( X ` x ) x. ( X ` y ) ) ) )
60 50 59 eqtr4d 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( 1 / ( X ` ( x ( .r ` Z ) y ) ) ) = ( ( 1 / ( X ` x ) ) x. ( 1 / ( X ` y ) ) ) )
61 34 8 sseldi 
 |-  ( ph -> X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) )
62 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
63 41 62 ringidval 
 |-  ( 1r ` Z ) = ( 0g ` ( mulGrp ` Z ) )
64 cnfld1 
 |-  1 = ( 1r ` CCfld )
65 45 64 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` CCfld ) )
66 63 65 mhm0 
 |-  ( X e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` CCfld ) ) -> ( X ` ( 1r ` Z ) ) = 1 )
67 61 66 syl 
 |-  ( ph -> ( X ` ( 1r ` Z ) ) = 1 )
68 67 oveq2d 
 |-  ( ph -> ( 1 / ( X ` ( 1r ` Z ) ) ) = ( 1 / 1 ) )
69 1div1e1 
 |-  ( 1 / 1 ) = 1
70 68 69 eqtrdi 
 |-  ( ph -> ( 1 / ( X ` ( 1r ` Z ) ) ) = 1 )
71 1 2 4 5 11 3 13 15 17 19 30 60 70 dchrelbasd 
 |-  ( ph -> ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) ) e. D )
72 9 71 eqeltrid 
 |-  ( ph -> K e. D )
73 1 2 3 7 72 8 dchrmul 
 |-  ( ph -> ( K .x. X ) = ( K oF x. X ) )
74 4 fvexi 
 |-  B e. _V
75 74 a1i 
 |-  ( ph -> B e. _V )
76 ovex 
 |-  ( 1 / ( X ` k ) ) e. _V
77 c0ex 
 |-  0 e. _V
78 76 77 ifex 
 |-  if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) e. _V
79 78 a1i 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) e. _V )
80 20 ffvelrnda 
 |-  ( ( ph /\ k e. B ) -> ( X ` k ) e. CC )
81 9 a1i 
 |-  ( ph -> K = ( k e. B |-> if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) ) )
82 20 feqmptd 
 |-  ( ph -> X = ( k e. B |-> ( X ` k ) ) )
83 75 79 80 81 82 offval2 
 |-  ( ph -> ( K oF x. X ) = ( k e. B |-> ( if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) x. ( X ` k ) ) ) )
84 ovif 
 |-  ( if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) x. ( X ` k ) ) = if ( k e. U , ( ( 1 / ( X ` k ) ) x. ( X ` k ) ) , ( 0 x. ( X ` k ) ) )
85 80 adantr 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> ( X ` k ) e. CC )
86 8 adantr 
 |-  ( ( ph /\ k e. B ) -> X e. D )
87 simpr 
 |-  ( ( ph /\ k e. B ) -> k e. B )
88 1 2 3 4 5 86 87 dchrn0 
 |-  ( ( ph /\ k e. B ) -> ( ( X ` k ) =/= 0 <-> k e. U ) )
89 88 biimpar 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> ( X ` k ) =/= 0 )
90 85 89 recid2d 
 |-  ( ( ( ph /\ k e. B ) /\ k e. U ) -> ( ( 1 / ( X ` k ) ) x. ( X ` k ) ) = 1 )
91 90 ifeq1da 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , ( ( 1 / ( X ` k ) ) x. ( X ` k ) ) , ( 0 x. ( X ` k ) ) ) = if ( k e. U , 1 , ( 0 x. ( X ` k ) ) ) )
92 80 mul02d 
 |-  ( ( ph /\ k e. B ) -> ( 0 x. ( X ` k ) ) = 0 )
93 92 ifeq2d 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , 1 , ( 0 x. ( X ` k ) ) ) = if ( k e. U , 1 , 0 ) )
94 91 93 eqtrd 
 |-  ( ( ph /\ k e. B ) -> if ( k e. U , ( ( 1 / ( X ` k ) ) x. ( X ` k ) ) , ( 0 x. ( X ` k ) ) ) = if ( k e. U , 1 , 0 ) )
95 84 94 syl5eq 
 |-  ( ( ph /\ k e. B ) -> ( if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) x. ( X ` k ) ) = if ( k e. U , 1 , 0 ) )
96 95 mpteq2dva 
 |-  ( ph -> ( k e. B |-> ( if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) x. ( X ` k ) ) ) = ( k e. B |-> if ( k e. U , 1 , 0 ) ) )
97 6 96 eqtr4id 
 |-  ( ph -> .1. = ( k e. B |-> ( if ( k e. U , ( 1 / ( X ` k ) ) , 0 ) x. ( X ` k ) ) ) )
98 83 97 eqtr4d 
 |-  ( ph -> ( K oF x. X ) = .1. )
99 73 98 eqtrd 
 |-  ( ph -> ( K .x. X ) = .1. )
100 72 99 jca 
 |-  ( ph -> ( K e. D /\ ( K .x. X ) = .1. ) )