Metamath Proof Explorer

Theorem dchrinv

Description: The inverse of a Dirichlet character is the conjugate (which is also the multiplicative inverse, because the values of X are unimodular). (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrabs.g 
|- G = ( DChr ` N )
dchrabs.d 
|- D = ( Base ` G )
dchrabs.x 
|- ( ph -> X e. D )
dchrinv.i 
|- I = ( invg ` G )
Assertion dchrinv 
|- ( ph -> ( I ` X ) = ( * o. X ) )

Proof

Step Hyp Ref Expression
1 dchrabs.g 
 |-  G = ( DChr ` N )
2 dchrabs.d 
 |-  D = ( Base ` G )
3 dchrabs.x 
 |-  ( ph -> X e. D )
4 dchrinv.i 
 |-  I = ( invg ` G )
5 eqid 
 |-  ( Z/nZ ` N ) = ( Z/nZ ` N )
6 eqid 
 |-  ( +g ` G ) = ( +g ` G )
7 cjf 
 |-  * : CC --> CC
8 eqid 
 |-  ( Base ` ( Z/nZ ` N ) ) = ( Base ` ( Z/nZ ` N ) )
9 1 5 2 8 3 dchrf 
 |-  ( ph -> X : ( Base ` ( Z/nZ ` N ) ) --> CC )
10 fco 
 |-  ( ( * : CC --> CC /\ X : ( Base ` ( Z/nZ ` N ) ) --> CC ) -> ( * o. X ) : ( Base ` ( Z/nZ ` N ) ) --> CC )
11 7 9 10 sylancr 
 |-  ( ph -> ( * o. X ) : ( Base ` ( Z/nZ ` N ) ) --> CC )
12 eqid 
 |-  ( Unit ` ( Z/nZ ` N ) ) = ( Unit ` ( Z/nZ ` N ) )
13 1 2 dchrrcl 
 |-  ( X e. D -> N e. NN )
14 3 13 syl 
 |-  ( ph -> N e. NN )
15 1 5 8 12 14 2 dchrelbas3 
 |-  ( ph -> ( X e. D <-> ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ ( A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) ) ) )
16 3 15 mpbid 
 |-  ( ph -> ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ ( A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) ) )
17 16 simprd 
 |-  ( ph -> ( A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) )
18 17 simp1d 
 |-  ( ph -> A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
19 18 r19.21bi 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> A. y e. ( Unit ` ( Z/nZ ` N ) ) ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
20 19 r19.21bi 
 |-  ( ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
21 20 anasss 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
22 21 fveq2d 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( * ` ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) ) = ( * ` ( ( X ` x ) x. ( X ` y ) ) ) )
23 9 adantr 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> X : ( Base ` ( Z/nZ ` N ) ) --> CC )
24 8 12 unitss 
 |-  ( Unit ` ( Z/nZ ` N ) ) C_ ( Base ` ( Z/nZ ` N ) )
25 simprl 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> x e. ( Unit ` ( Z/nZ ` N ) ) )
26 24 25 sseldi 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> x e. ( Base ` ( Z/nZ ` N ) ) )
27 23 26 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( X ` x ) e. CC )
28 simprr 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> y e. ( Unit ` ( Z/nZ ` N ) ) )
29 24 28 sseldi 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> y e. ( Base ` ( Z/nZ ` N ) ) )
30 23 29 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( X ` y ) e. CC )
31 27 30 cjmuld 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( * ` ( ( X ` x ) x. ( X ` y ) ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
32 22 31 eqtrd 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( * ` ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
33 14 nnnn0d 
 |-  ( ph -> N e. NN0 )
34 5 zncrng 
 |-  ( N e. NN0 -> ( Z/nZ ` N ) e. CRing )
35 crngring 
 |-  ( ( Z/nZ ` N ) e. CRing -> ( Z/nZ ` N ) e. Ring )
36 33 34 35 3syl 
 |-  ( ph -> ( Z/nZ ` N ) e. Ring )
37 36 adantr 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( Z/nZ ` N ) e. Ring )
38 eqid 
 |-  ( .r ` ( Z/nZ ` N ) ) = ( .r ` ( Z/nZ ` N ) )
39 8 38 ringcl 
 |-  ( ( ( Z/nZ ` N ) e. Ring /\ x e. ( Base ` ( Z/nZ ` N ) ) /\ y e. ( Base ` ( Z/nZ ` N ) ) ) -> ( x ( .r ` ( Z/nZ ` N ) ) y ) e. ( Base ` ( Z/nZ ` N ) ) )
40 37 26 29 39 syl3anc 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( x ( .r ` ( Z/nZ ` N ) ) y ) e. ( Base ` ( Z/nZ ` N ) ) )
41 fvco3 
 |-  ( ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ ( x ( .r ` ( Z/nZ ` N ) ) y ) e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( * ` ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) ) )
42 23 40 41 syl2anc 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( * ` ( X ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) ) )
43 fvco3 
 |-  ( ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
44 23 26 43 syl2anc 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
45 fvco3 
 |-  ( ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ y e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` y ) = ( * ` ( X ` y ) ) )
46 23 29 45 syl2anc 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( ( * o. X ) ` y ) = ( * ` ( X ` y ) ) )
47 44 46 oveq12d 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) = ( ( * ` ( X ` x ) ) x. ( * ` ( X ` y ) ) ) )
48 32 42 47 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Unit ` ( Z/nZ ` N ) ) /\ y e. ( Unit ` ( Z/nZ ` N ) ) ) ) -> ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) )
49 48 ralrimivva 
 |-  ( ph -> A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) )
50 eqid 
 |-  ( 1r ` ( Z/nZ ` N ) ) = ( 1r ` ( Z/nZ ` N ) )
51 8 50 ringidcl 
 |-  ( ( Z/nZ ` N ) e. Ring -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
52 36 51 syl 
 |-  ( ph -> ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) )
53 fvco3 
 |-  ( ( X : ( Base ` ( Z/nZ ` N ) ) --> CC /\ ( 1r ` ( Z/nZ ` N ) ) e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` ( 1r ` ( Z/nZ ` N ) ) ) = ( * ` ( X ` ( 1r ` ( Z/nZ ` N ) ) ) ) )
54 9 52 53 syl2anc 
 |-  ( ph -> ( ( * o. X ) ` ( 1r ` ( Z/nZ ` N ) ) ) = ( * ` ( X ` ( 1r ` ( Z/nZ ` N ) ) ) ) )
55 17 simp2d 
 |-  ( ph -> ( X ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 )
56 55 fveq2d 
 |-  ( ph -> ( * ` ( X ` ( 1r ` ( Z/nZ ` N ) ) ) ) = ( * ` 1 ) )
57 1re 
 |-  1 e. RR
58 cjre 
 |-  ( 1 e. RR -> ( * ` 1 ) = 1 )
59 57 58 ax-mp 
 |-  ( * ` 1 ) = 1
60 56 59 eqtrdi 
 |-  ( ph -> ( * ` ( X ` ( 1r ` ( Z/nZ ` N ) ) ) ) = 1 )
61 54 60 eqtrd 
 |-  ( ph -> ( ( * o. X ) ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 )
62 17 simp3d 
 |-  ( ph -> A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) )
63 9 43 sylan 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
64 cj0 
 |-  ( * ` 0 ) = 0
65 64 eqcomi 
 |-  0 = ( * ` 0 )
66 65 a1i 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> 0 = ( * ` 0 ) )
67 63 66 eqeq12d 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( ( * o. X ) ` x ) = 0 <-> ( * ` ( X ` x ) ) = ( * ` 0 ) ) )
68 9 ffvelrnda 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( X ` x ) e. CC )
69 0cn 
 |-  0 e. CC
70 cj11 
 |-  ( ( ( X ` x ) e. CC /\ 0 e. CC ) -> ( ( * ` ( X ` x ) ) = ( * ` 0 ) <-> ( X ` x ) = 0 ) )
71 68 69 70 sylancl 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( * ` ( X ` x ) ) = ( * ` 0 ) <-> ( X ` x ) = 0 ) )
72 67 71 bitrd 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( ( * o. X ) ` x ) = 0 <-> ( X ` x ) = 0 ) )
73 72 necon3bid 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( ( * o. X ) ` x ) =/= 0 <-> ( X ` x ) =/= 0 ) )
74 73 imbi1d 
 |-  ( ( ph /\ x e. ( Base ` ( Z/nZ ` N ) ) ) -> ( ( ( ( * o. X ) ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) <-> ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) )
75 74 ralbidva 
 |-  ( ph -> ( A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) <-> A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( X ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) )
76 62 75 mpbird 
 |-  ( ph -> A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) )
77 49 61 76 3jca 
 |-  ( ph -> ( A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) /\ ( ( * o. X ) ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) )
78 1 5 8 12 14 2 dchrelbas3 
 |-  ( ph -> ( ( * o. X ) e. D <-> ( ( * o. X ) : ( Base ` ( Z/nZ ` N ) ) --> CC /\ ( A. x e. ( Unit ` ( Z/nZ ` N ) ) A. y e. ( Unit ` ( Z/nZ ` N ) ) ( ( * o. X ) ` ( x ( .r ` ( Z/nZ ` N ) ) y ) ) = ( ( ( * o. X ) ` x ) x. ( ( * o. X ) ` y ) ) /\ ( ( * o. X ) ` ( 1r ` ( Z/nZ ` N ) ) ) = 1 /\ A. x e. ( Base ` ( Z/nZ ` N ) ) ( ( ( * o. X ) ` x ) =/= 0 -> x e. ( Unit ` ( Z/nZ ` N ) ) ) ) ) ) )
79 11 77 78 mpbir2and 
 |-  ( ph -> ( * o. X ) e. D )
80 1 5 2 6 3 79 dchrmul 
 |-  ( ph -> ( X ( +g ` G ) ( * o. X ) ) = ( X oF x. ( * o. X ) ) )
81 80 adantr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( X ( +g ` G ) ( * o. X ) ) = ( X oF x. ( * o. X ) ) )
82 81 fveq1d 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( X oF x. ( * o. X ) ) ` x ) )
83 24 sseli 
 |-  ( x e. ( Unit ` ( Z/nZ ` N ) ) -> x e. ( Base ` ( Z/nZ ` N ) ) )
84 83 63 sylan2 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( * o. X ) ` x ) = ( * ` ( X ` x ) ) )
85 84 oveq2d 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X ` x ) x. ( ( * o. X ) ` x ) ) = ( ( X ` x ) x. ( * ` ( X ` x ) ) ) )
86 83 68 sylan2 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( X ` x ) e. CC )
87 86 absvalsqd 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = ( ( X ` x ) x. ( * ` ( X ` x ) ) ) )
88 3 adantr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> X e. D )
89 simpr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> x e. ( Unit ` ( Z/nZ ` N ) ) )
90 1 2 88 5 12 89 dchrabs 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( abs ` ( X ` x ) ) = 1 )
91 90 oveq1d 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = ( 1 ^ 2 ) )
92 sq1 
 |-  ( 1 ^ 2 ) = 1
93 91 92 eqtrdi 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( abs ` ( X ` x ) ) ^ 2 ) = 1 )
94 85 87 93 3eqtr2d 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X ` x ) x. ( ( * o. X ) ` x ) ) = 1 )
95 9 adantr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> X : ( Base ` ( Z/nZ ` N ) ) --> CC )
96 95 ffnd 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> X Fn ( Base ` ( Z/nZ ` N ) ) )
97 11 ffnd 
 |-  ( ph -> ( * o. X ) Fn ( Base ` ( Z/nZ ` N ) ) )
98 97 adantr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( * o. X ) Fn ( Base ` ( Z/nZ ` N ) ) )
99 fvexd 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( Base ` ( Z/nZ ` N ) ) e. _V )
100 83 adantl 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> x e. ( Base ` ( Z/nZ ` N ) ) )
101 fnfvof 
 |-  ( ( ( X Fn ( Base ` ( Z/nZ ` N ) ) /\ ( * o. X ) Fn ( Base ` ( Z/nZ ` N ) ) ) /\ ( ( Base ` ( Z/nZ ` N ) ) e. _V /\ x e. ( Base ` ( Z/nZ ` N ) ) ) ) -> ( ( X oF x. ( * o. X ) ) ` x ) = ( ( X ` x ) x. ( ( * o. X ) ` x ) ) )
102 96 98 99 100 101 syl22anc 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X oF x. ( * o. X ) ) ` x ) = ( ( X ` x ) x. ( ( * o. X ) ` x ) ) )
103 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
104 14 adantr 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> N e. NN )
105 1 5 103 12 104 89 dchr1 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( 0g ` G ) ` x ) = 1 )
106 94 102 105 3eqtr4d 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X oF x. ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
107 82 106 eqtrd 
 |-  ( ( ph /\ x e. ( Unit ` ( Z/nZ ` N ) ) ) -> ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
108 107 ralrimiva 
 |-  ( ph -> A. x e. ( Unit ` ( Z/nZ ` N ) ) ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) )
109 1 5 2 6 3 79 dchrmulcl 
 |-  ( ph -> ( X ( +g ` G ) ( * o. X ) ) e. D )
110 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
111 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
112 14 110 111 3syl 
 |-  ( ph -> G e. Grp )
113 2 103 grpidcl 
 |-  ( G e. Grp -> ( 0g ` G ) e. D )
114 112 113 syl 
 |-  ( ph -> ( 0g ` G ) e. D )
115 1 5 2 12 109 114 dchreq 
 |-  ( ph -> ( ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) <-> A. x e. ( Unit ` ( Z/nZ ` N ) ) ( ( X ( +g ` G ) ( * o. X ) ) ` x ) = ( ( 0g ` G ) ` x ) ) )
116 108 115 mpbird 
 |-  ( ph -> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) )
117 2 6 103 4 grpinvid1 
 |-  ( ( G e. Grp /\ X e. D /\ ( * o. X ) e. D ) -> ( ( I ` X ) = ( * o. X ) <-> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) ) )
118 112 3 79 117 syl3anc 
 |-  ( ph -> ( ( I ` X ) = ( * o. X ) <-> ( X ( +g ` G ) ( * o. X ) ) = ( 0g ` G ) ) )
119 116 118 mpbird 
 |-  ( ph -> ( I ` X ) = ( * o. X ) )