Metamath Proof Explorer

Theorem psgnunilem4

Description: Lemma for psgnuni . An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses psgnunilem4.g 
|- G = ( SymGrp ` D )
psgnunilem4.t 
|- T = ran ( pmTrsp ` D )
psgnunilem4.d 
|- ( ph -> D e. V )
psgnunilem4.w1 
|- ( ph -> W e. Word T )
psgnunilem4.w2 
|- ( ph -> ( G gsum W ) = ( _I |` D ) )
Assertion psgnunilem4 
|- ( ph -> ( -u 1 ^ ( # ` W ) ) = 1 )

Proof

Step Hyp Ref Expression
1 psgnunilem4.g 
 |-  G = ( SymGrp ` D )
2 psgnunilem4.t 
 |-  T = ran ( pmTrsp ` D )
3 psgnunilem4.d 
 |-  ( ph -> D e. V )
4 psgnunilem4.w1 
 |-  ( ph -> W e. Word T )
5 psgnunilem4.w2 
 |-  ( ph -> ( G gsum W ) = ( _I |` D ) )
6 wrdfin 
 |-  ( W e. Word T -> W e. Fin )
7 hashcl 
 |-  ( W e. Fin -> ( # ` W ) e. NN0 )
8 4 6 7 3syl 
 |-  ( ph -> ( # ` W ) e. NN0 )
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 8 9 eleqtrdi 
 |-  ( ph -> ( # ` W ) e. ( ZZ>= ` 0 ) )
11 fveq2 
 |-  ( w = (/) -> ( # ` w ) = ( # ` (/) ) )
12 hash0 
 |-  ( # ` (/) ) = 0
13 11 12 eqtrdi 
 |-  ( w = (/) -> ( # ` w ) = 0 )
14 13 oveq2d 
 |-  ( w = (/) -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ 0 ) )
15 neg1cn 
 |-  -u 1 e. CC
16 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
17 15 16 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
18 14 17 eqtrdi 
 |-  ( w = (/) -> ( -u 1 ^ ( # ` w ) ) = 1 )
19 18 2a1d 
 |-  ( w = (/) -> ( ( ph /\ A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
20 simpl1 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ph )
21 20 3 syl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> D e. V )
22 simpl3l 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> w e. Word T )
23 eqidd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( # ` w ) = ( # ` w ) )
24 wrdfin 
 |-  ( w e. Word T -> w e. Fin )
25 22 24 syl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> w e. Fin )
26 simpl2 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> w =/= (/) )
27 hashnncl 
 |-  ( w e. Fin -> ( ( # ` w ) e. NN <-> w =/= (/) ) )
28 27 biimpar 
 |-  ( ( w e. Fin /\ w =/= (/) ) -> ( # ` w ) e. NN )
29 25 26 28 syl2anc 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( # ` w ) e. NN )
30 simpl3r 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( G gsum w ) = ( _I |` D ) )
31 fveqeq2 
 |-  ( x = y -> ( ( # ` x ) = ( ( # ` w ) - 2 ) <-> ( # ` y ) = ( ( # ` w ) - 2 ) ) )
32 oveq2 
 |-  ( x = y -> ( G gsum x ) = ( G gsum y ) )
33 32 eqeq1d 
 |-  ( x = y -> ( ( G gsum x ) = ( _I |` D ) <-> ( G gsum y ) = ( _I |` D ) ) )
34 31 33 anbi12d 
 |-  ( x = y -> ( ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> ( ( # ` y ) = ( ( # ` w ) - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) ) )
35 34 cbvrexvw 
 |-  ( E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> E. y e. Word T ( ( # ` y ) = ( ( # ` w ) - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
36 35 notbii 
 |-  ( -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> -. E. y e. Word T ( ( # ` y ) = ( ( # ` w ) - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
37 36 biimpi 
 |-  ( -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) -> -. E. y e. Word T ( ( # ` y ) = ( ( # ` w ) - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
38 37 adantl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> -. E. y e. Word T ( ( # ` y ) = ( ( # ` w ) - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
39 1 2 21 22 23 29 30 38 psgnunilem3 
 |-  -. ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
40 iman 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) <-> -. ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ -. E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) )
41 39 40 mpbir 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
42 df-rex 
 |-  ( E. x e. Word T ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> E. x ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) )
43 41 42 sylib 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> E. x ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) )
44 simprl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> x e. Word T )
45 simprrr 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( G gsum x ) = ( _I |` D ) )
46 44 45 jca 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) )
47 wrdfin 
 |-  ( x e. Word T -> x e. Fin )
48 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
49 44 47 48 3syl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` x ) e. NN0 )
50 simp3l 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> w e. Word T )
51 50 24 syl 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> w e. Fin )
52 simp2 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> w =/= (/) )
53 51 52 28 syl2anc 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( # ` w ) e. NN )
54 53 adantr 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` w ) e. NN )
55 simprrl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` x ) = ( ( # ` w ) - 2 ) )
56 54 nnred 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` w ) e. RR )
57 2rp 
 |-  2 e. RR+
58 ltsubrp 
 |-  ( ( ( # ` w ) e. RR /\ 2 e. RR+ ) -> ( ( # ` w ) - 2 ) < ( # ` w ) )
59 56 57 58 sylancl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( # ` w ) - 2 ) < ( # ` w ) )
60 55 59 eqbrtrd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` x ) < ( # ` w ) )
61 elfzo0 
 |-  ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) <-> ( ( # ` x ) e. NN0 /\ ( # ` w ) e. NN /\ ( # ` x ) < ( # ` w ) ) )
62 49 54 60 61 syl3anbrc 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` x ) e. ( 0 ..^ ( # ` w ) ) )
63 id 
 |-  ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) )
64 63 com13 
 |-  ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) )
65 46 62 64 sylc 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) )
66 55 oveq2d 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( -u 1 ^ ( # ` x ) ) = ( -u 1 ^ ( ( # ` w ) - 2 ) ) )
67 15 a1i 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> -u 1 e. CC )
68 neg1ne0 
 |-  -u 1 =/= 0
69 68 a1i 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> -u 1 =/= 0 )
70 2z 
 |-  2 e. ZZ
71 70 a1i 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> 2 e. ZZ )
72 54 nnzd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( # ` w ) e. ZZ )
73 67 69 71 72 expsubd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( -u 1 ^ ( ( # ` w ) - 2 ) ) = ( ( -u 1 ^ ( # ` w ) ) / ( -u 1 ^ 2 ) ) )
74 neg1sqe1 
 |-  ( -u 1 ^ 2 ) = 1
75 74 oveq2i 
 |-  ( ( -u 1 ^ ( # ` w ) ) / ( -u 1 ^ 2 ) ) = ( ( -u 1 ^ ( # ` w ) ) / 1 )
76 m1expcl 
 |-  ( ( # ` w ) e. ZZ -> ( -u 1 ^ ( # ` w ) ) e. ZZ )
77 76 zcnd 
 |-  ( ( # ` w ) e. ZZ -> ( -u 1 ^ ( # ` w ) ) e. CC )
78 72 77 syl 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( -u 1 ^ ( # ` w ) ) e. CC )
79 78 div1d 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( -u 1 ^ ( # ` w ) ) / 1 ) = ( -u 1 ^ ( # ` w ) ) )
80 75 79 syl5eq 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( -u 1 ^ ( # ` w ) ) / ( -u 1 ^ 2 ) ) = ( -u 1 ^ ( # ` w ) ) )
81 66 73 80 3eqtrd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( -u 1 ^ ( # ` x ) ) = ( -u 1 ^ ( # ` w ) ) )
82 81 eqeq1d 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( -u 1 ^ ( # ` x ) ) = 1 <-> ( -u 1 ^ ( # ` w ) ) = 1 ) )
83 65 82 sylibd 
 |-  ( ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) /\ ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) ) -> ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) )
84 83 ex 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
85 84 com23 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
86 85 alimdv 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> A. x ( ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
87 19.23v 
 |-  ( A. x ( ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) <-> ( E. x ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) )
88 86 87 syl6ib 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( E. x ( x e. Word T /\ ( ( # ` x ) = ( ( # ` w ) - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
89 43 88 mpid 
 |-  ( ( ph /\ w =/= (/) /\ ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) ) -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) )
90 89 3exp 
 |-  ( ph -> ( w =/= (/) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) ) )
91 90 com34 
 |-  ( ph -> ( w =/= (/) -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) ) )
92 91 com12 
 |-  ( w =/= (/) -> ( ph -> ( A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) ) )
93 92 impd 
 |-  ( w =/= (/) -> ( ( ph /\ A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) ) )
94 19 93 pm2.61ine 
 |-  ( ( ph /\ A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) )
95 94 3adant2 
 |-  ( ( ph /\ ( # ` w ) e. ( 0 ... ( # ` W ) ) /\ A. x ( ( # ` x ) e. ( 0 ..^ ( # ` w ) ) -> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) ) -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) )
96 eleq1 
 |-  ( w = x -> ( w e. Word T <-> x e. Word T ) )
97 oveq2 
 |-  ( w = x -> ( G gsum w ) = ( G gsum x ) )
98 97 eqeq1d 
 |-  ( w = x -> ( ( G gsum w ) = ( _I |` D ) <-> ( G gsum x ) = ( _I |` D ) ) )
99 96 98 anbi12d 
 |-  ( w = x -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) <-> ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) ) )
100 fveq2 
 |-  ( w = x -> ( # ` w ) = ( # ` x ) )
101 100 oveq2d 
 |-  ( w = x -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` x ) ) )
102 101 eqeq1d 
 |-  ( w = x -> ( ( -u 1 ^ ( # ` w ) ) = 1 <-> ( -u 1 ^ ( # ` x ) ) = 1 ) )
103 99 102 imbi12d 
 |-  ( w = x -> ( ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) <-> ( ( x e. Word T /\ ( G gsum x ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` x ) ) = 1 ) ) )
104 eleq1 
 |-  ( w = W -> ( w e. Word T <-> W e. Word T ) )
105 oveq2 
 |-  ( w = W -> ( G gsum w ) = ( G gsum W ) )
106 105 eqeq1d 
 |-  ( w = W -> ( ( G gsum w ) = ( _I |` D ) <-> ( G gsum W ) = ( _I |` D ) ) )
107 104 106 anbi12d 
 |-  ( w = W -> ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) <-> ( W e. Word T /\ ( G gsum W ) = ( _I |` D ) ) ) )
108 fveq2 
 |-  ( w = W -> ( # ` w ) = ( # ` W ) )
109 108 oveq2d 
 |-  ( w = W -> ( -u 1 ^ ( # ` w ) ) = ( -u 1 ^ ( # ` W ) ) )
110 109 eqeq1d 
 |-  ( w = W -> ( ( -u 1 ^ ( # ` w ) ) = 1 <-> ( -u 1 ^ ( # ` W ) ) = 1 ) )
111 107 110 imbi12d 
 |-  ( w = W -> ( ( ( w e. Word T /\ ( G gsum w ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` w ) ) = 1 ) <-> ( ( W e. Word T /\ ( G gsum W ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` W ) ) = 1 ) ) )
112 4 10 95 103 111 100 108 uzindi 
 |-  ( ph -> ( ( W e. Word T /\ ( G gsum W ) = ( _I |` D ) ) -> ( -u 1 ^ ( # ` W ) ) = 1 ) )
113 4 5 112 mp2and 
 |-  ( ph -> ( -u 1 ^ ( # ` W ) ) = 1 )