Metamath Proof Explorer

Theorem dchrptlem2

Description: Lemma for dchrpt . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrpt.g 
|- G = ( DChr ` N )
dchrpt.z 
|- Z = ( Z/nZ ` N )
dchrpt.d 
|- D = ( Base ` G )
dchrpt.b 
|- B = ( Base ` Z )
dchrpt.1 
|- .1. = ( 1r ` Z )
dchrpt.n 
|- ( ph -> N e. NN )
dchrpt.n1 
|- ( ph -> A =/= .1. )
dchrpt.u 
|- U = ( Unit ` Z )
dchrpt.h 
|- H = ( ( mulGrp ` Z ) |`s U )
dchrpt.m 
|- .x. = ( .g ` H )
dchrpt.s 
|- S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )
dchrpt.au 
|- ( ph -> A e. U )
dchrpt.w 
|- ( ph -> W e. Word U )
dchrpt.2 
|- ( ph -> H dom DProd S )
dchrpt.3 
|- ( ph -> ( H DProd S ) = U )
dchrpt.p 
|- P = ( H dProj S )
dchrpt.o 
|- O = ( od ` H )
dchrpt.t 
|- T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )
dchrpt.i 
|- ( ph -> I e. dom W )
dchrpt.4 
|- ( ph -> ( ( P ` I ) ` A ) =/= .1. )
dchrpt.5 
|- X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
Assertion dchrptlem2 
|- ( ph -> E. x e. D ( x ` A ) =/= 1 )

Proof

Step Hyp Ref Expression
1 dchrpt.g 
 |-  G = ( DChr ` N )
2 dchrpt.z 
 |-  Z = ( Z/nZ ` N )
3 dchrpt.d 
 |-  D = ( Base ` G )
4 dchrpt.b 
 |-  B = ( Base ` Z )
5 dchrpt.1 
 |-  .1. = ( 1r ` Z )
6 dchrpt.n 
 |-  ( ph -> N e. NN )
7 dchrpt.n1 
 |-  ( ph -> A =/= .1. )
8 dchrpt.u 
 |-  U = ( Unit ` Z )
9 dchrpt.h 
 |-  H = ( ( mulGrp ` Z ) |`s U )
10 dchrpt.m 
 |-  .x. = ( .g ` H )
11 dchrpt.s 
 |-  S = ( k e. dom W |-> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) )
12 dchrpt.au 
 |-  ( ph -> A e. U )
13 dchrpt.w 
 |-  ( ph -> W e. Word U )
14 dchrpt.2 
 |-  ( ph -> H dom DProd S )
15 dchrpt.3 
 |-  ( ph -> ( H DProd S ) = U )
16 dchrpt.p 
 |-  P = ( H dProj S )
17 dchrpt.o 
 |-  O = ( od ` H )
18 dchrpt.t 
 |-  T = ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) )
19 dchrpt.i 
 |-  ( ph -> I e. dom W )
20 dchrpt.4 
 |-  ( ph -> ( ( P ` I ) ` A ) =/= .1. )
21 dchrpt.5 
 |-  X = ( u e. U |-> ( iota h E. m e. ZZ ( ( ( P ` I ) ` u ) = ( m .x. ( W ` I ) ) /\ h = ( T ^ m ) ) ) )
22 fveq2 
 |-  ( v = x -> ( X ` v ) = ( X ` x ) )
23 fveq2 
 |-  ( v = y -> ( X ` v ) = ( X ` y ) )
24 fveq2 
 |-  ( v = ( x ( .r ` Z ) y ) -> ( X ` v ) = ( X ` ( x ( .r ` Z ) y ) ) )
25 fveq2 
 |-  ( v = ( 1r ` Z ) -> ( X ` v ) = ( X ` ( 1r ` Z ) ) )
26 zex 
 |-  ZZ e. _V
27 26 mptex 
 |-  ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) e. _V
28 27 rnex 
 |-  ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) e. _V
29 28 11 dmmpti 
 |-  dom S = dom W
30 29 a1i 
 |-  ( ph -> dom S = dom W )
31 14 30 16 19 dpjf 
 |-  ( ph -> ( P ` I ) : ( H DProd S ) --> ( S ` I ) )
32 15 feq2d 
 |-  ( ph -> ( ( P ` I ) : ( H DProd S ) --> ( S ` I ) <-> ( P ` I ) : U --> ( S ` I ) ) )
33 31 32 mpbid 
 |-  ( ph -> ( P ` I ) : U --> ( S ` I ) )
34 33 ffvelcdmda 
 |-  ( ( ph /\ v e. U ) -> ( ( P ` I ) ` v ) e. ( S ` I ) )
35 19 adantr 
 |-  ( ( ph /\ v e. U ) -> I e. dom W )
36 oveq1 
 |-  ( n = a -> ( n .x. ( W ` k ) ) = ( a .x. ( W ` k ) ) )
37 36 cbvmptv 
 |-  ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) = ( a e. ZZ |-> ( a .x. ( W ` k ) ) )
38 fveq2 
 |-  ( k = I -> ( W ` k ) = ( W ` I ) )
39 38 oveq2d 
 |-  ( k = I -> ( a .x. ( W ` k ) ) = ( a .x. ( W ` I ) ) )
40 39 mpteq2dv 
 |-  ( k = I -> ( a e. ZZ |-> ( a .x. ( W ` k ) ) ) = ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
41 37 40 eqtrid 
 |-  ( k = I -> ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) = ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
42 41 rneqd 
 |-  ( k = I -> ran ( n e. ZZ |-> ( n .x. ( W ` k ) ) ) = ran ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
43 42 11 28 fvmpt3i 
 |-  ( I e. dom W -> ( S ` I ) = ran ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
44 35 43 syl 
 |-  ( ( ph /\ v e. U ) -> ( S ` I ) = ran ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
45 34 44 eleqtrd 
 |-  ( ( ph /\ v e. U ) -> ( ( P ` I ) ` v ) e. ran ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) )
46 eqid 
 |-  ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) = ( a e. ZZ |-> ( a .x. ( W ` I ) ) )
47 ovex 
 |-  ( a .x. ( W ` I ) ) e. _V
48 46 47 elrnmpti 
 |-  ( ( ( P ` I ) ` v ) e. ran ( a e. ZZ |-> ( a .x. ( W ` I ) ) ) <-> E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) )
49 45 48 sylib 
 |-  ( ( ph /\ v e. U ) -> E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` v ) = ( T ^ a ) )
51 neg1cn 
 |-  -u 1 e. CC
52 2re 
 |-  2 e. RR
53 6 nnnn0d 
 |-  ( ph -> N e. NN0 )
54 2 zncrng 
 |-  ( N e. NN0 -> Z e. CRing )
55 crngring 
 |-  ( Z e. CRing -> Z e. Ring )
56 53 54 55 3syl 
 |-  ( ph -> Z e. Ring )
57 8 9 unitgrp 
 |-  ( Z e. Ring -> H e. Grp )
58 56 57 syl 
 |-  ( ph -> H e. Grp )
59 2 4 znfi 
 |-  ( N e. NN -> B e. Fin )
60 6 59 syl 
 |-  ( ph -> B e. Fin )
61 4 8 unitss 
 |-  U C_ B
62 ssfi 
 |-  ( ( B e. Fin /\ U C_ B ) -> U e. Fin )
63 60 61 62 sylancl 
 |-  ( ph -> U e. Fin )
64 wrdf 
 |-  ( W e. Word U -> W : ( 0 ..^ ( # ` W ) ) --> U )
65 13 64 syl 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> U )
66 65 fdmd 
 |-  ( ph -> dom W = ( 0 ..^ ( # ` W ) ) )
67 19 66 eleqtrd 
 |-  ( ph -> I e. ( 0 ..^ ( # ` W ) ) )
68 65 67 ffvelcdmd 
 |-  ( ph -> ( W ` I ) e. U )
69 8 9 unitgrpbas 
 |-  U = ( Base ` H )
70 69 17 odcl2 
 |-  ( ( H e. Grp /\ U e. Fin /\ ( W ` I ) e. U ) -> ( O ` ( W ` I ) ) e. NN )
71 58 63 68 70 syl3anc 
 |-  ( ph -> ( O ` ( W ` I ) ) e. NN )
72 nndivre 
 |-  ( ( 2 e. RR /\ ( O ` ( W ` I ) ) e. NN ) -> ( 2 / ( O ` ( W ` I ) ) ) e. RR )
73 52 71 72 sylancr 
 |-  ( ph -> ( 2 / ( O ` ( W ` I ) ) ) e. RR )
74 73 recnd 
 |-  ( ph -> ( 2 / ( O ` ( W ` I ) ) ) e. CC )
75 cxpcl 
 |-  ( ( -u 1 e. CC /\ ( 2 / ( O ` ( W ` I ) ) ) e. CC ) -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) e. CC )
76 51 74 75 sylancr 
 |-  ( ph -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) e. CC )
77 18 76 eqeltrid 
 |-  ( ph -> T e. CC )
78 77 ad2antrr 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> T e. CC )
79 51 a1i 
 |-  ( ph -> -u 1 e. CC )
80 neg1ne0 
 |-  -u 1 =/= 0
81 80 a1i 
 |-  ( ph -> -u 1 =/= 0 )
82 79 81 74 cxpne0d 
 |-  ( ph -> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) =/= 0 )
83 18 neeq1i 
 |-  ( T =/= 0 <-> ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) =/= 0 )
84 82 83 sylibr 
 |-  ( ph -> T =/= 0 )
85 84 ad2antrr 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> T =/= 0 )
86 simprl 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> a e. ZZ )
87 78 85 86 expclzd 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> ( T ^ a ) e. CC )
88 50 87 eqeltrd 
 |-  ( ( ( ph /\ v e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` v ) e. CC )
89 49 88 rexlimddv 
 |-  ( ( ph /\ v e. U ) -> ( X ` v ) e. CC )
90 fveqeq2 
 |-  ( v = x -> ( ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) ) )
91 90 rexbidv 
 |-  ( v = x -> ( E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> E. a e. ZZ ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) ) )
92 49 ralrimiva 
 |-  ( ph -> A. v e. U E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) )
93 92 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> A. v e. U E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) )
94 simprl 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. U )
95 91 93 94 rspcdva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> E. a e. ZZ ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) )
96 fveqeq2 
 |-  ( v = y -> ( ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> ( ( P ` I ) ` y ) = ( a .x. ( W ` I ) ) ) )
97 96 rexbidv 
 |-  ( v = y -> ( E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> E. a e. ZZ ( ( P ` I ) ` y ) = ( a .x. ( W ` I ) ) ) )
98 oveq1 
 |-  ( a = b -> ( a .x. ( W ` I ) ) = ( b .x. ( W ` I ) ) )
99 98 eqeq2d 
 |-  ( a = b -> ( ( ( P ` I ) ` y ) = ( a .x. ( W ` I ) ) <-> ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) )
100 99 cbvrexvw 
 |-  ( E. a e. ZZ ( ( P ` I ) ` y ) = ( a .x. ( W ` I ) ) <-> E. b e. ZZ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) )
101 97 100 bitrdi 
 |-  ( v = y -> ( E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> E. b e. ZZ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) )
102 simprr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. U )
103 101 93 102 rspcdva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> E. b e. ZZ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) )
104 reeanv 
 |-  ( E. a e. ZZ E. b e. ZZ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) <-> ( E. a e. ZZ ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ E. b e. ZZ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) )
105 77 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> T e. CC )
106 84 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> T =/= 0 )
107 simprll 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> a e. ZZ )
108 simprlr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> b e. ZZ )
109 expaddz 
 |-  ( ( ( T e. CC /\ T =/= 0 ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( T ^ ( a + b ) ) = ( ( T ^ a ) x. ( T ^ b ) ) )
110 105 106 107 108 109 syl22anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( T ^ ( a + b ) ) = ( ( T ^ a ) x. ( T ^ b ) ) )
111 simpll 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ph )
112 56 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> Z e. Ring )
113 94 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> x e. U )
114 102 adantr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> y e. U )
115 eqid 
 |-  ( .r ` Z ) = ( .r ` Z )
116 8 115 unitmulcl 
 |-  ( ( Z e. Ring /\ x e. U /\ y e. U ) -> ( x ( .r ` Z ) y ) e. U )
117 112 113 114 116 syl3anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( x ( .r ` Z ) y ) e. U )
118 107 108 zaddcld 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( a + b ) e. ZZ )
119 simprrl 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) )
120 simprrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) )
121 119 120 oveq12d 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( ( P ` I ) ` x ) ( .r ` Z ) ( ( P ` I ) ` y ) ) = ( ( a .x. ( W ` I ) ) ( .r ` Z ) ( b .x. ( W ` I ) ) ) )
122 14 30 16 19 dpjghm 
 |-  ( ph -> ( P ` I ) e. ( ( H |`s ( H DProd S ) ) GrpHom H ) )
123 15 oveq2d 
 |-  ( ph -> ( H |`s ( H DProd S ) ) = ( H |`s U ) )
124 9 ovexi 
 |-  H e. _V
125 69 ressid 
 |-  ( H e. _V -> ( H |`s U ) = H )
126 124 125 ax-mp 
 |-  ( H |`s U ) = H
127 123 126 eqtrdi 
 |-  ( ph -> ( H |`s ( H DProd S ) ) = H )
128 127 oveq1d 
 |-  ( ph -> ( ( H |`s ( H DProd S ) ) GrpHom H ) = ( H GrpHom H ) )
129 122 128 eleqtrd 
 |-  ( ph -> ( P ` I ) e. ( H GrpHom H ) )
130 129 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( P ` I ) e. ( H GrpHom H ) )
131 8 fvexi 
 |-  U e. _V
132 eqid 
 |-  ( mulGrp ` Z ) = ( mulGrp ` Z )
133 132 115 mgpplusg 
 |-  ( .r ` Z ) = ( +g ` ( mulGrp ` Z ) )
134 9 133 ressplusg 
 |-  ( U e. _V -> ( .r ` Z ) = ( +g ` H ) )
135 131 134 ax-mp 
 |-  ( .r ` Z ) = ( +g ` H )
136 69 135 135 ghmlin 
 |-  ( ( ( P ` I ) e. ( H GrpHom H ) /\ x e. U /\ y e. U ) -> ( ( P ` I ) ` ( x ( .r ` Z ) y ) ) = ( ( ( P ` I ) ` x ) ( .r ` Z ) ( ( P ` I ) ` y ) ) )
137 130 113 114 136 syl3anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( P ` I ) ` ( x ( .r ` Z ) y ) ) = ( ( ( P ` I ) ` x ) ( .r ` Z ) ( ( P ` I ) ` y ) ) )
138 58 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> H e. Grp )
139 68 ad2antrr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( W ` I ) e. U )
140 69 10 135 mulgdir 
 |-  ( ( H e. Grp /\ ( a e. ZZ /\ b e. ZZ /\ ( W ` I ) e. U ) ) -> ( ( a + b ) .x. ( W ` I ) ) = ( ( a .x. ( W ` I ) ) ( .r ` Z ) ( b .x. ( W ` I ) ) ) )
141 138 107 108 139 140 syl13anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( a + b ) .x. ( W ` I ) ) = ( ( a .x. ( W ` I ) ) ( .r ` Z ) ( b .x. ( W ` I ) ) ) )
142 121 137 141 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( P ` I ) ` ( x ( .r ` Z ) y ) ) = ( ( a + b ) .x. ( W ` I ) ) )
143 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ ( x ( .r ` Z ) y ) e. U ) /\ ( ( a + b ) e. ZZ /\ ( ( P ` I ) ` ( x ( .r ` Z ) y ) ) = ( ( a + b ) .x. ( W ` I ) ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( T ^ ( a + b ) ) )
144 111 117 118 142 143 syl22anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( T ^ ( a + b ) ) )
145 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ x e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` x ) = ( T ^ a ) )
146 111 113 107 119 145 syl22anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( X ` x ) = ( T ^ a ) )
147 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ y e. U ) /\ ( b e. ZZ /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) -> ( X ` y ) = ( T ^ b ) )
148 111 114 108 120 147 syl22anc 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( X ` y ) = ( T ^ b ) )
149 146 148 oveq12d 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( ( X ` x ) x. ( X ` y ) ) = ( ( T ^ a ) x. ( T ^ b ) ) )
150 110 144 149 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( ( a e. ZZ /\ b e. ZZ ) /\ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
151 150 expr 
 |-  ( ( ( ph /\ ( x e. U /\ y e. U ) ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
152 151 rexlimdvva 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( E. a e. ZZ E. b e. ZZ ( ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
153 104 152 biimtrrid 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( ( E. a e. ZZ ( ( P ` I ) ` x ) = ( a .x. ( W ` I ) ) /\ E. b e. ZZ ( ( P ` I ) ` y ) = ( b .x. ( W ` I ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
154 95 103 153 mp2and 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
155 id 
 |-  ( ph -> ph )
156 eqid 
 |-  ( 1r ` Z ) = ( 1r ` Z )
157 8 156 1unit 
 |-  ( Z e. Ring -> ( 1r ` Z ) e. U )
158 56 157 syl 
 |-  ( ph -> ( 1r ` Z ) e. U )
159 0zd 
 |-  ( ph -> 0 e. ZZ )
160 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
161 160 160 ghmid 
 |-  ( ( P ` I ) e. ( H GrpHom H ) -> ( ( P ` I ) ` ( 0g ` H ) ) = ( 0g ` H ) )
162 129 161 syl 
 |-  ( ph -> ( ( P ` I ) ` ( 0g ` H ) ) = ( 0g ` H ) )
163 8 9 156 unitgrpid 
 |-  ( Z e. Ring -> ( 1r ` Z ) = ( 0g ` H ) )
164 56 163 syl 
 |-  ( ph -> ( 1r ` Z ) = ( 0g ` H ) )
165 164 fveq2d 
 |-  ( ph -> ( ( P ` I ) ` ( 1r ` Z ) ) = ( ( P ` I ) ` ( 0g ` H ) ) )
166 69 160 10 mulg0 
 |-  ( ( W ` I ) e. U -> ( 0 .x. ( W ` I ) ) = ( 0g ` H ) )
167 68 166 syl 
 |-  ( ph -> ( 0 .x. ( W ` I ) ) = ( 0g ` H ) )
168 162 165 167 3eqtr4d 
 |-  ( ph -> ( ( P ` I ) ` ( 1r ` Z ) ) = ( 0 .x. ( W ` I ) ) )
169 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ ( 1r ` Z ) e. U ) /\ ( 0 e. ZZ /\ ( ( P ` I ) ` ( 1r ` Z ) ) = ( 0 .x. ( W ` I ) ) ) ) -> ( X ` ( 1r ` Z ) ) = ( T ^ 0 ) )
170 155 158 159 168 169 syl22anc 
 |-  ( ph -> ( X ` ( 1r ` Z ) ) = ( T ^ 0 ) )
171 77 exp0d 
 |-  ( ph -> ( T ^ 0 ) = 1 )
172 170 171 eqtrd 
 |-  ( ph -> ( X ` ( 1r ` Z ) ) = 1 )
173 1 2 4 8 6 3 22 23 24 25 89 154 172 dchrelbasd 
 |-  ( ph -> ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) e. D )
174 61 12 sselid 
 |-  ( ph -> A e. B )
175 eleq1 
 |-  ( v = A -> ( v e. U <-> A e. U ) )
176 fveq2 
 |-  ( v = A -> ( X ` v ) = ( X ` A ) )
177 175 176 ifbieq1d 
 |-  ( v = A -> if ( v e. U , ( X ` v ) , 0 ) = if ( A e. U , ( X ` A ) , 0 ) )
178 eqid 
 |-  ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) = ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) )
179 fvex 
 |-  ( X ` v ) e. _V
180 c0ex 
 |-  0 e. _V
181 179 180 ifex 
 |-  if ( v e. U , ( X ` v ) , 0 ) e. _V
182 177 178 181 fvmpt3i 
 |-  ( A e. B -> ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) = if ( A e. U , ( X ` A ) , 0 ) )
183 174 182 syl 
 |-  ( ph -> ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) = if ( A e. U , ( X ` A ) , 0 ) )
184 12 iftrued 
 |-  ( ph -> if ( A e. U , ( X ` A ) , 0 ) = ( X ` A ) )
185 183 184 eqtrd 
 |-  ( ph -> ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) = ( X ` A ) )
186 fveqeq2 
 |-  ( v = A -> ( ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) )
187 186 rexbidv 
 |-  ( v = A -> ( E. a e. ZZ ( ( P ` I ) ` v ) = ( a .x. ( W ` I ) ) <-> E. a e. ZZ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) )
188 187 92 12 rspcdva 
 |-  ( ph -> E. a e. ZZ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) )
189 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 dchrptlem1 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` A ) = ( T ^ a ) )
190 18 oveq1i 
 |-  ( T ^ a ) = ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a )
191 189 190 eqtrdi 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` A ) = ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) )
192 20 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( P ` I ) ` A ) =/= .1. )
193 58 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> H e. Grp )
194 68 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( W ` I ) e. U )
195 simprl 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> a e. ZZ )
196 69 17 10 160 oddvds 
 |-  ( ( H e. Grp /\ ( W ` I ) e. U /\ a e. ZZ ) -> ( ( O ` ( W ` I ) ) || a <-> ( a .x. ( W ` I ) ) = ( 0g ` H ) ) )
197 193 194 195 196 syl3anc 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( O ` ( W ` I ) ) || a <-> ( a .x. ( W ` I ) ) = ( 0g ` H ) ) )
198 71 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( O ` ( W ` I ) ) e. NN )
199 root1eq1 
 |-  ( ( ( O ` ( W ` I ) ) e. NN /\ a e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) = 1 <-> ( O ` ( W ` I ) ) || a ) )
200 198 195 199 syl2anc 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) = 1 <-> ( O ` ( W ` I ) ) || a ) )
201 simprr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) )
202 5 164 eqtrid 
 |-  ( ph -> .1. = ( 0g ` H ) )
203 202 ad2antrr 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> .1. = ( 0g ` H ) )
204 201 203 eqeq12d 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( ( P ` I ) ` A ) = .1. <-> ( a .x. ( W ` I ) ) = ( 0g ` H ) ) )
205 197 200 204 3bitr4d 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) = 1 <-> ( ( P ` I ) ` A ) = .1. ) )
206 205 necon3bid 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) =/= 1 <-> ( ( P ` I ) ` A ) =/= .1. ) )
207 192 206 mpbird 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( ( -u 1 ^c ( 2 / ( O ` ( W ` I ) ) ) ) ^ a ) =/= 1 )
208 191 207 eqnetrd 
 |-  ( ( ( ph /\ A e. U ) /\ ( a e. ZZ /\ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) ) ) -> ( X ` A ) =/= 1 )
209 208 rexlimdvaa 
 |-  ( ( ph /\ A e. U ) -> ( E. a e. ZZ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) -> ( X ` A ) =/= 1 ) )
210 12 209 mpdan 
 |-  ( ph -> ( E. a e. ZZ ( ( P ` I ) ` A ) = ( a .x. ( W ` I ) ) -> ( X ` A ) =/= 1 ) )
211 188 210 mpd 
 |-  ( ph -> ( X ` A ) =/= 1 )
212 185 211 eqnetrd 
 |-  ( ph -> ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) =/= 1 )
213 fveq1 
 |-  ( x = ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) -> ( x ` A ) = ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) )
214 213 neeq1d 
 |-  ( x = ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) -> ( ( x ` A ) =/= 1 <-> ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) =/= 1 ) )
215 214 rspcev 
 |-  ( ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) e. D /\ ( ( v e. B |-> if ( v e. U , ( X ` v ) , 0 ) ) ` A ) =/= 1 ) -> E. x e. D ( x ` A ) =/= 1 )
216 173 212 215 syl2anc 
 |-  ( ph -> E. x e. D ( x ` A ) =/= 1 )