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 ffvelrnda
 |-  ( ( 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 syl5eq
 |-  ( 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 ffvelrnd
 |-  ( 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 syl5bir
 |-  ( ( 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 syl5eq
 |-  ( 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 )