Metamath Proof Explorer

Theorem psgnunilem3

Description: Lemma for psgnuni . Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015)

Ref Expression
Hypotheses psgnunilem3.g 
|- G = ( SymGrp ` D )
psgnunilem3.t 
|- T = ran ( pmTrsp ` D )
psgnunilem3.d 
|- ( ph -> D e. V )
psgnunilem3.w1 
|- ( ph -> W e. Word T )
psgnunilem3.l 
|- ( ph -> ( # ` W ) = L )
psgnunilem3.w2 
|- ( ph -> ( # ` W ) e. NN )
psgnunilem3.w3 
|- ( ph -> ( G gsum W ) = ( _I |` D ) )
psgnunilem3.in 
|- ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
Assertion psgnunilem3 
|- -. ph

Proof

Step Hyp Ref Expression
1 psgnunilem3.g 
 |-  G = ( SymGrp ` D )
2 psgnunilem3.t 
 |-  T = ran ( pmTrsp ` D )
3 psgnunilem3.d 
 |-  ( ph -> D e. V )
4 psgnunilem3.w1 
 |-  ( ph -> W e. Word T )
5 psgnunilem3.l 
 |-  ( ph -> ( # ` W ) = L )
6 psgnunilem3.w2 
 |-  ( ph -> ( # ` W ) e. NN )
7 psgnunilem3.w3 
 |-  ( ph -> ( G gsum W ) = ( _I |` D ) )
8 psgnunilem3.in 
 |-  ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
9 5 6 eqeltrrd 
 |-  ( ph -> L e. NN )
10 9 nnnn0d 
 |-  ( ph -> L e. NN0 )
11 wrdf 
 |-  ( W e. Word T -> W : ( 0 ..^ ( # ` W ) ) --> T )
12 4 11 syl 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> T )
13 0nn0 
 |-  0 e. NN0
14 13 a1i 
 |-  ( ph -> 0 e. NN0 )
15 9 nngt0d 
 |-  ( ph -> 0 < L )
16 elfzo0 
 |-  ( 0 e. ( 0 ..^ L ) <-> ( 0 e. NN0 /\ L e. NN /\ 0 < L ) )
17 14 9 15 16 syl3anbrc 
 |-  ( ph -> 0 e. ( 0 ..^ L ) )
18 5 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ L ) )
19 17 18 eleqtrrd 
 |-  ( ph -> 0 e. ( 0 ..^ ( # ` W ) ) )
20 12 19 ffvelrnd 
 |-  ( ph -> ( W ` 0 ) e. T )
21 eqid 
 |-  ( pmTrsp ` D ) = ( pmTrsp ` D )
22 21 2 pmtrfmvdn0 
 |-  ( ( W ` 0 ) e. T -> dom ( ( W ` 0 ) \ _I ) =/= (/) )
23 20 22 syl 
 |-  ( ph -> dom ( ( W ` 0 ) \ _I ) =/= (/) )
24 n0 
 |-  ( dom ( ( W ` 0 ) \ _I ) =/= (/) <-> E. e e e. dom ( ( W ` 0 ) \ _I ) )
25 23 24 sylib 
 |-  ( ph -> E. e e e. dom ( ( W ` 0 ) \ _I ) )
26 fzonel 
 |-  -. L e. ( 0 ..^ L )
27 simpr1 
 |-  ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) -> L e. ( 0 ..^ L ) )
28 26 27 mto 
 |-  -. ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) )
29 28 a1i 
 |-  ( w e. Word T -> -. ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
30 29 nrex 
 |-  -. E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) )
31 eleq1 
 |-  ( a = 0 -> ( a e. ( 0 ..^ L ) <-> 0 e. ( 0 ..^ L ) ) )
32 fveq2 
 |-  ( a = 0 -> ( w ` a ) = ( w ` 0 ) )
33 32 difeq1d 
 |-  ( a = 0 -> ( ( w ` a ) \ _I ) = ( ( w ` 0 ) \ _I ) )
34 33 dmeqd 
 |-  ( a = 0 -> dom ( ( w ` a ) \ _I ) = dom ( ( w ` 0 ) \ _I ) )
35 34 eleq2d 
 |-  ( a = 0 -> ( e e. dom ( ( w ` a ) \ _I ) <-> e e. dom ( ( w ` 0 ) \ _I ) ) )
36 oveq2 
 |-  ( a = 0 -> ( 0 ..^ a ) = ( 0 ..^ 0 ) )
37 36 raleqdv 
 |-  ( a = 0 -> ( A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) )
38 31 35 37 3anbi123d 
 |-  ( a = 0 -> ( ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
39 38 anbi2d 
 |-  ( a = 0 -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
40 39 rexbidv 
 |-  ( a = 0 -> ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
41 40 imbi2d 
 |-  ( a = 0 -> ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) <-> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) ) )
42 eleq1 
 |-  ( a = b -> ( a e. ( 0 ..^ L ) <-> b e. ( 0 ..^ L ) ) )
43 fveq2 
 |-  ( a = b -> ( w ` a ) = ( w ` b ) )
44 43 difeq1d 
 |-  ( a = b -> ( ( w ` a ) \ _I ) = ( ( w ` b ) \ _I ) )
45 44 dmeqd 
 |-  ( a = b -> dom ( ( w ` a ) \ _I ) = dom ( ( w ` b ) \ _I ) )
46 45 eleq2d 
 |-  ( a = b -> ( e e. dom ( ( w ` a ) \ _I ) <-> e e. dom ( ( w ` b ) \ _I ) ) )
47 oveq2 
 |-  ( a = b -> ( 0 ..^ a ) = ( 0 ..^ b ) )
48 47 raleqdv 
 |-  ( a = b -> ( A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) )
49 42 46 48 3anbi123d 
 |-  ( a = b -> ( ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
50 49 anbi2d 
 |-  ( a = b -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
51 50 rexbidv 
 |-  ( a = b -> ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
52 oveq2 
 |-  ( w = x -> ( G gsum w ) = ( G gsum x ) )
53 52 eqeq1d 
 |-  ( w = x -> ( ( G gsum w ) = ( _I |` D ) <-> ( G gsum x ) = ( _I |` D ) ) )
54 fveqeq2 
 |-  ( w = x -> ( ( # ` w ) = L <-> ( # ` x ) = L ) )
55 53 54 anbi12d 
 |-  ( w = x -> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) <-> ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) ) )
56 fveq1 
 |-  ( w = x -> ( w ` b ) = ( x ` b ) )
57 56 difeq1d 
 |-  ( w = x -> ( ( w ` b ) \ _I ) = ( ( x ` b ) \ _I ) )
58 57 dmeqd 
 |-  ( w = x -> dom ( ( w ` b ) \ _I ) = dom ( ( x ` b ) \ _I ) )
59 58 eleq2d 
 |-  ( w = x -> ( e e. dom ( ( w ` b ) \ _I ) <-> e e. dom ( ( x ` b ) \ _I ) ) )
60 fveq1 
 |-  ( w = x -> ( w ` c ) = ( x ` c ) )
61 60 difeq1d 
 |-  ( w = x -> ( ( w ` c ) \ _I ) = ( ( x ` c ) \ _I ) )
62 61 dmeqd 
 |-  ( w = x -> dom ( ( w ` c ) \ _I ) = dom ( ( x ` c ) \ _I ) )
63 62 eleq2d 
 |-  ( w = x -> ( e e. dom ( ( w ` c ) \ _I ) <-> e e. dom ( ( x ` c ) \ _I ) ) )
64 63 notbid 
 |-  ( w = x -> ( -. e e. dom ( ( w ` c ) \ _I ) <-> -. e e. dom ( ( x ` c ) \ _I ) ) )
65 64 ralbidv 
 |-  ( w = x -> ( A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ b ) -. e e. dom ( ( x ` c ) \ _I ) ) )
66 fveq2 
 |-  ( c = d -> ( x ` c ) = ( x ` d ) )
67 66 difeq1d 
 |-  ( c = d -> ( ( x ` c ) \ _I ) = ( ( x ` d ) \ _I ) )
68 67 dmeqd 
 |-  ( c = d -> dom ( ( x ` c ) \ _I ) = dom ( ( x ` d ) \ _I ) )
69 68 eleq2d 
 |-  ( c = d -> ( e e. dom ( ( x ` c ) \ _I ) <-> e e. dom ( ( x ` d ) \ _I ) ) )
70 69 notbid 
 |-  ( c = d -> ( -. e e. dom ( ( x ` c ) \ _I ) <-> -. e e. dom ( ( x ` d ) \ _I ) ) )
71 70 cbvralvw 
 |-  ( A. c e. ( 0 ..^ b ) -. e e. dom ( ( x ` c ) \ _I ) <-> A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) )
72 65 71 bitrdi 
 |-  ( w = x -> ( A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) )
73 59 72 3anbi23d 
 |-  ( w = x -> ( ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) )
74 55 73 anbi12d 
 |-  ( w = x -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) )
75 74 cbvrexvw 
 |-  ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( w ` b ) \ _I ) /\ A. c e. ( 0 ..^ b ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) )
76 51 75 bitrdi 
 |-  ( a = b -> ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) )
77 76 imbi2d 
 |-  ( a = b -> ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) <-> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) )
78 eleq1 
 |-  ( a = ( b + 1 ) -> ( a e. ( 0 ..^ L ) <-> ( b + 1 ) e. ( 0 ..^ L ) ) )
79 fveq2 
 |-  ( a = ( b + 1 ) -> ( w ` a ) = ( w ` ( b + 1 ) ) )
80 79 difeq1d 
 |-  ( a = ( b + 1 ) -> ( ( w ` a ) \ _I ) = ( ( w ` ( b + 1 ) ) \ _I ) )
81 80 dmeqd 
 |-  ( a = ( b + 1 ) -> dom ( ( w ` a ) \ _I ) = dom ( ( w ` ( b + 1 ) ) \ _I ) )
82 81 eleq2d 
 |-  ( a = ( b + 1 ) -> ( e e. dom ( ( w ` a ) \ _I ) <-> e e. dom ( ( w ` ( b + 1 ) ) \ _I ) ) )
83 oveq2 
 |-  ( a = ( b + 1 ) -> ( 0 ..^ a ) = ( 0 ..^ ( b + 1 ) ) )
84 83 raleqdv 
 |-  ( a = ( b + 1 ) -> ( A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) )
85 78 82 84 3anbi123d 
 |-  ( a = ( b + 1 ) -> ( ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
86 85 anbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
87 86 rexbidv 
 |-  ( a = ( b + 1 ) -> ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
88 87 imbi2d 
 |-  ( a = ( b + 1 ) -> ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) <-> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) ) )
89 eleq1 
 |-  ( a = L -> ( a e. ( 0 ..^ L ) <-> L e. ( 0 ..^ L ) ) )
90 fveq2 
 |-  ( a = L -> ( w ` a ) = ( w ` L ) )
91 90 difeq1d 
 |-  ( a = L -> ( ( w ` a ) \ _I ) = ( ( w ` L ) \ _I ) )
92 91 dmeqd 
 |-  ( a = L -> dom ( ( w ` a ) \ _I ) = dom ( ( w ` L ) \ _I ) )
93 92 eleq2d 
 |-  ( a = L -> ( e e. dom ( ( w ` a ) \ _I ) <-> e e. dom ( ( w ` L ) \ _I ) ) )
94 oveq2 
 |-  ( a = L -> ( 0 ..^ a ) = ( 0 ..^ L ) )
95 94 raleqdv 
 |-  ( a = L -> ( A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) )
96 89 93 95 3anbi123d 
 |-  ( a = L -> ( ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
97 96 anbi2d 
 |-  ( a = L -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
98 97 rexbidv 
 |-  ( a = L -> ( E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
99 98 imbi2d 
 |-  ( a = L -> ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( a e. ( 0 ..^ L ) /\ e e. dom ( ( w ` a ) \ _I ) /\ A. c e. ( 0 ..^ a ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) <-> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) ) )
100 4 adantr 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> W e. Word T )
101 7 5 jca 
 |-  ( ph -> ( ( G gsum W ) = ( _I |` D ) /\ ( # ` W ) = L ) )
102 101 adantr 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> ( ( G gsum W ) = ( _I |` D ) /\ ( # ` W ) = L ) )
103 17 adantr 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> 0 e. ( 0 ..^ L ) )
104 simpr 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> e e. dom ( ( W ` 0 ) \ _I ) )
105 ral0 
 |-  A. c e. (/) -. e e. dom ( ( W ` c ) \ _I )
106 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
107 106 raleqi 
 |-  ( A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) <-> A. c e. (/) -. e e. dom ( ( W ` c ) \ _I ) )
108 105 107 mpbir 
 |-  A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I )
109 108 a1i 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) )
110 103 104 109 3jca 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( W ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) ) )
111 oveq2 
 |-  ( w = W -> ( G gsum w ) = ( G gsum W ) )
112 111 eqeq1d 
 |-  ( w = W -> ( ( G gsum w ) = ( _I |` D ) <-> ( G gsum W ) = ( _I |` D ) ) )
113 fveqeq2 
 |-  ( w = W -> ( ( # ` w ) = L <-> ( # ` W ) = L ) )
114 112 113 anbi12d 
 |-  ( w = W -> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) <-> ( ( G gsum W ) = ( _I |` D ) /\ ( # ` W ) = L ) ) )
115 fveq1 
 |-  ( w = W -> ( w ` 0 ) = ( W ` 0 ) )
116 115 difeq1d 
 |-  ( w = W -> ( ( w ` 0 ) \ _I ) = ( ( W ` 0 ) \ _I ) )
117 116 dmeqd 
 |-  ( w = W -> dom ( ( w ` 0 ) \ _I ) = dom ( ( W ` 0 ) \ _I ) )
118 117 eleq2d 
 |-  ( w = W -> ( e e. dom ( ( w ` 0 ) \ _I ) <-> e e. dom ( ( W ` 0 ) \ _I ) ) )
119 fveq1 
 |-  ( w = W -> ( w ` c ) = ( W ` c ) )
120 119 difeq1d 
 |-  ( w = W -> ( ( w ` c ) \ _I ) = ( ( W ` c ) \ _I ) )
121 120 dmeqd 
 |-  ( w = W -> dom ( ( w ` c ) \ _I ) = dom ( ( W ` c ) \ _I ) )
122 121 eleq2d 
 |-  ( w = W -> ( e e. dom ( ( w ` c ) \ _I ) <-> e e. dom ( ( W ` c ) \ _I ) ) )
123 122 notbid 
 |-  ( w = W -> ( -. e e. dom ( ( w ` c ) \ _I ) <-> -. e e. dom ( ( W ` c ) \ _I ) ) )
124 123 ralbidv 
 |-  ( w = W -> ( A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) <-> A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) ) )
125 118 124 3anbi23d 
 |-  ( w = W -> ( ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) <-> ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( W ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) ) ) )
126 114 125 anbi12d 
 |-  ( w = W -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) <-> ( ( ( G gsum W ) = ( _I |` D ) /\ ( # ` W ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( W ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) ) ) ) )
127 126 rspcev 
 |-  ( ( W e. Word T /\ ( ( ( G gsum W ) = ( _I |` D ) /\ ( # ` W ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( W ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( W ` c ) \ _I ) ) ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
128 100 102 110 127 syl12anc 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( 0 e. ( 0 ..^ L ) /\ e e. dom ( ( w ` 0 ) \ _I ) /\ A. c e. ( 0 ..^ 0 ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
129 3 ad2antrr 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> D e. V )
130 simprl 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> x e. Word T )
131 simpll 
 |-  ( ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> ( G gsum x ) = ( _I |` D ) )
132 131 ad2antll 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> ( G gsum x ) = ( _I |` D ) )
133 simplr 
 |-  ( ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> ( # ` x ) = L )
134 133 ad2antll 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> ( # ` x ) = L )
135 simpr1 
 |-  ( ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> b e. ( 0 ..^ L ) )
136 135 ad2antll 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> b e. ( 0 ..^ L ) )
137 simpr2 
 |-  ( ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> e e. dom ( ( x ` b ) \ _I ) )
138 137 ad2antll 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> e e. dom ( ( x ` b ) \ _I ) )
139 simpr3 
 |-  ( ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) )
140 139 ad2antll 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) )
141 fveqeq2 
 |-  ( x = y -> ( ( # ` x ) = ( L - 2 ) <-> ( # ` y ) = ( L - 2 ) ) )
142 oveq2 
 |-  ( x = y -> ( G gsum x ) = ( G gsum y ) )
143 142 eqeq1d 
 |-  ( x = y -> ( ( G gsum x ) = ( _I |` D ) <-> ( G gsum y ) = ( _I |` D ) ) )
144 141 143 anbi12d 
 |-  ( x = y -> ( ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> ( ( # ` y ) = ( L - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) ) )
145 144 cbvrexvw 
 |-  ( E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> E. y e. Word T ( ( # ` y ) = ( L - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
146 8 145 sylnib 
 |-  ( ph -> -. E. y e. Word T ( ( # ` y ) = ( L - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
147 146 ad2antrr 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> -. E. y e. Word T ( ( # ` y ) = ( L - 2 ) /\ ( G gsum y ) = ( _I |` D ) ) )
148 1 2 129 130 132 134 136 138 140 147 psgnunilem2 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) /\ ( x e. Word T /\ ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) )
149 148 rexlimdvaa 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> ( E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
150 149 a2i 
 |-  ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) -> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
151 150 a1i 
 |-  ( b e. NN0 -> ( ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. x e. Word T ( ( ( G gsum x ) = ( _I |` D ) /\ ( # ` x ) = L ) /\ ( b e. ( 0 ..^ L ) /\ e e. dom ( ( x ` b ) \ _I ) /\ A. d e. ( 0 ..^ b ) -. e e. dom ( ( x ` d ) \ _I ) ) ) ) -> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( b + 1 ) e. ( 0 ..^ L ) /\ e e. dom ( ( w ` ( b + 1 ) ) \ _I ) /\ A. c e. ( 0 ..^ ( b + 1 ) ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) ) )
152 41 77 88 99 128 151 nn0ind 
 |-  ( L e. NN0 -> ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( L e. ( 0 ..^ L ) /\ e e. dom ( ( w ` L ) \ _I ) /\ A. c e. ( 0 ..^ L ) -. e e. dom ( ( w ` c ) \ _I ) ) ) ) )
153 30 152 mtoi 
 |-  ( L e. NN0 -> -. ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) )
154 153 con2i 
 |-  ( ( ph /\ e e. dom ( ( W ` 0 ) \ _I ) ) -> -. L e. NN0 )
155 25 154 exlimddv 
 |-  ( ph -> -. L e. NN0 )
156 10 155 pm2.65i 
 |-  -. ph