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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 sselid
 |-  ( ( 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 sselid
 |-  ( 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. ) )