Metamath Proof Explorer

Theorem psgnunilem2

Description: Lemma for psgnuni . Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by Mario Carneiro, 28-Feb-2016)

Ref Expression
Hypotheses psgnunilem2.g 
|- G = ( SymGrp ` D )
psgnunilem2.t 
|- T = ran ( pmTrsp ` D )
psgnunilem2.d 
|- ( ph -> D e. V )
psgnunilem2.w 
|- ( ph -> W e. Word T )
psgnunilem2.id 
|- ( ph -> ( G gsum W ) = ( _I |` D ) )
psgnunilem2.l 
|- ( ph -> ( # ` W ) = L )
psgnunilem2.ix 
|- ( ph -> I e. ( 0 ..^ L ) )
psgnunilem2.a 
|- ( ph -> A e. dom ( ( W ` I ) \ _I ) )
psgnunilem2.al 
|- ( ph -> A. k e. ( 0 ..^ I ) -. A e. dom ( ( W ` k ) \ _I ) )
psgnunilem2.in 
|- ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
Assertion psgnunilem2 
|- ( ph -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )

Proof

Step Hyp Ref Expression
1 psgnunilem2.g 
 |-  G = ( SymGrp ` D )
2 psgnunilem2.t 
 |-  T = ran ( pmTrsp ` D )
3 psgnunilem2.d 
 |-  ( ph -> D e. V )
4 psgnunilem2.w 
 |-  ( ph -> W e. Word T )
5 psgnunilem2.id 
 |-  ( ph -> ( G gsum W ) = ( _I |` D ) )
6 psgnunilem2.l 
 |-  ( ph -> ( # ` W ) = L )
7 psgnunilem2.ix 
 |-  ( ph -> I e. ( 0 ..^ L ) )
8 psgnunilem2.a 
 |-  ( ph -> A e. dom ( ( W ` I ) \ _I ) )
9 psgnunilem2.al 
 |-  ( ph -> A. k e. ( 0 ..^ I ) -. A e. dom ( ( W ` k ) \ _I ) )
10 psgnunilem2.in 
 |-  ( ph -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
11 wrd0 
 |-  (/) e. Word T
12 splcl 
 |-  ( ( W e. Word T /\ (/) e. Word T ) -> ( W splice <. I , ( I + 2 ) , (/) >. ) e. Word T )
13 4 11 12 sylancl 
 |-  ( ph -> ( W splice <. I , ( I + 2 ) , (/) >. ) e. Word T )
14 13 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( W splice <. I , ( I + 2 ) , (/) >. ) e. Word T )
15 fzossfz 
 |-  ( 0 ..^ L ) C_ ( 0 ... L )
16 15 7 sselid 
 |-  ( ph -> I e. ( 0 ... L ) )
17 elfznn0 
 |-  ( I e. ( 0 ... L ) -> I e. NN0 )
18 16 17 syl 
 |-  ( ph -> I e. NN0 )
19 2nn0 
 |-  2 e. NN0
20 nn0addcl 
 |-  ( ( I e. NN0 /\ 2 e. NN0 ) -> ( I + 2 ) e. NN0 )
21 18 19 20 sylancl 
 |-  ( ph -> ( I + 2 ) e. NN0 )
22 18 nn0red 
 |-  ( ph -> I e. RR )
23 nn0addge1 
 |-  ( ( I e. RR /\ 2 e. NN0 ) -> I <_ ( I + 2 ) )
24 22 19 23 sylancl 
 |-  ( ph -> I <_ ( I + 2 ) )
25 elfz2nn0 
 |-  ( I e. ( 0 ... ( I + 2 ) ) <-> ( I e. NN0 /\ ( I + 2 ) e. NN0 /\ I <_ ( I + 2 ) ) )
26 18 21 24 25 syl3anbrc 
 |-  ( ph -> I e. ( 0 ... ( I + 2 ) ) )
27 1 2 3 4 5 6 7 8 9 psgnunilem5 
 |-  ( ph -> ( I + 1 ) e. ( 0 ..^ L ) )
28 fzofzp1 
 |-  ( ( I + 1 ) e. ( 0 ..^ L ) -> ( ( I + 1 ) + 1 ) e. ( 0 ... L ) )
29 27 28 syl 
 |-  ( ph -> ( ( I + 1 ) + 1 ) e. ( 0 ... L ) )
30 df-2 
 |-  2 = ( 1 + 1 )
31 30 oveq2i 
 |-  ( I + 2 ) = ( I + ( 1 + 1 ) )
32 18 nn0cnd 
 |-  ( ph -> I e. CC )
33 1cnd 
 |-  ( ph -> 1 e. CC )
34 32 33 33 addassd 
 |-  ( ph -> ( ( I + 1 ) + 1 ) = ( I + ( 1 + 1 ) ) )
35 31 34 eqtr4id 
 |-  ( ph -> ( I + 2 ) = ( ( I + 1 ) + 1 ) )
36 6 oveq2d 
 |-  ( ph -> ( 0 ... ( # ` W ) ) = ( 0 ... L ) )
37 29 35 36 3eltr4d 
 |-  ( ph -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
38 11 a1i 
 |-  ( ph -> (/) e. Word T )
39 4 26 37 38 spllen 
 |-  ( ph -> ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( ( # ` W ) + ( ( # ` (/) ) - ( ( I + 2 ) - I ) ) ) )
40 hash0 
 |-  ( # ` (/) ) = 0
41 40 oveq1i 
 |-  ( ( # ` (/) ) - ( ( I + 2 ) - I ) ) = ( 0 - ( ( I + 2 ) - I ) )
42 df-neg 
 |-  -u ( ( I + 2 ) - I ) = ( 0 - ( ( I + 2 ) - I ) )
43 41 42 eqtr4i 
 |-  ( ( # ` (/) ) - ( ( I + 2 ) - I ) ) = -u ( ( I + 2 ) - I )
44 2cn 
 |-  2 e. CC
45 pncan2 
 |-  ( ( I e. CC /\ 2 e. CC ) -> ( ( I + 2 ) - I ) = 2 )
46 32 44 45 sylancl 
 |-  ( ph -> ( ( I + 2 ) - I ) = 2 )
47 46 negeqd 
 |-  ( ph -> -u ( ( I + 2 ) - I ) = -u 2 )
48 43 47 eqtrid 
 |-  ( ph -> ( ( # ` (/) ) - ( ( I + 2 ) - I ) ) = -u 2 )
49 6 48 oveq12d 
 |-  ( ph -> ( ( # ` W ) + ( ( # ` (/) ) - ( ( I + 2 ) - I ) ) ) = ( L + -u 2 ) )
50 elfzel2 
 |-  ( I e. ( 0 ... L ) -> L e. ZZ )
51 16 50 syl 
 |-  ( ph -> L e. ZZ )
52 51 zcnd 
 |-  ( ph -> L e. CC )
53 negsub 
 |-  ( ( L e. CC /\ 2 e. CC ) -> ( L + -u 2 ) = ( L - 2 ) )
54 52 44 53 sylancl 
 |-  ( ph -> ( L + -u 2 ) = ( L - 2 ) )
55 39 49 54 3eqtrd 
 |-  ( ph -> ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) )
56 55 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) )
57 splid 
 |-  ( ( W e. Word T /\ ( I e. ( 0 ... ( I + 2 ) ) /\ ( I + 2 ) e. ( 0 ... ( # ` W ) ) ) ) -> ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) = W )
58 4 26 37 57 syl12anc 
 |-  ( ph -> ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) = W )
59 58 oveq2d 
 |-  ( ph -> ( G gsum ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) ) = ( G gsum W ) )
60 59 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) ) = ( G gsum W ) )
61 eqid 
 |-  ( Base ` G ) = ( Base ` G )
62 1 symggrp 
 |-  ( D e. V -> G e. Grp )
63 3 62 syl 
 |-  ( ph -> G e. Grp )
64 63 grpmndd 
 |-  ( ph -> G e. Mnd )
65 64 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> G e. Mnd )
66 2 1 61 symgtrf 
 |-  T C_ ( Base ` G )
67 sswrd 
 |-  ( T C_ ( Base ` G ) -> Word T C_ Word ( Base ` G ) )
68 66 67 ax-mp 
 |-  Word T C_ Word ( Base ` G )
69 68 4 sselid 
 |-  ( ph -> W e. Word ( Base ` G ) )
70 69 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> W e. Word ( Base ` G ) )
71 26 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> I e. ( 0 ... ( I + 2 ) ) )
72 37 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
73 swrdcl 
 |-  ( W e. Word ( Base ` G ) -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
74 69 73 syl 
 |-  ( ph -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
75 74 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
76 wrd0 
 |-  (/) e. Word ( Base ` G )
77 76 a1i 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> (/) e. Word ( Base ` G ) )
78 6 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ L ) )
79 27 78 eleqtrrd 
 |-  ( ph -> ( I + 1 ) e. ( 0 ..^ ( # ` W ) ) )
80 swrds2 
 |-  ( ( W e. Word T /\ I e. NN0 /\ ( I + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
81 4 18 79 80 syl3anc 
 |-  ( ph -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
82 81 oveq2d 
 |-  ( ph -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( G gsum <" ( W ` I ) ( W ` ( I + 1 ) ) "> ) )
83 wrdf 
 |-  ( W e. Word T -> W : ( 0 ..^ ( # ` W ) ) --> T )
84 4 83 syl 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> T )
85 78 feq2d 
 |-  ( ph -> ( W : ( 0 ..^ ( # ` W ) ) --> T <-> W : ( 0 ..^ L ) --> T ) )
86 84 85 mpbid 
 |-  ( ph -> W : ( 0 ..^ L ) --> T )
87 86 7 ffvelrnd 
 |-  ( ph -> ( W ` I ) e. T )
88 66 87 sselid 
 |-  ( ph -> ( W ` I ) e. ( Base ` G ) )
89 86 27 ffvelrnd 
 |-  ( ph -> ( W ` ( I + 1 ) ) e. T )
90 66 89 sselid 
 |-  ( ph -> ( W ` ( I + 1 ) ) e. ( Base ` G ) )
91 eqid 
 |-  ( +g ` G ) = ( +g ` G )
92 61 91 gsumws2 
 |-  ( ( G e. Mnd /\ ( W ` I ) e. ( Base ` G ) /\ ( W ` ( I + 1 ) ) e. ( Base ` G ) ) -> ( G gsum <" ( W ` I ) ( W ` ( I + 1 ) ) "> ) = ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) )
93 64 88 90 92 syl3anc 
 |-  ( ph -> ( G gsum <" ( W ` I ) ( W ` ( I + 1 ) ) "> ) = ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) )
94 1 61 91 symgov 
 |-  ( ( ( W ` I ) e. ( Base ` G ) /\ ( W ` ( I + 1 ) ) e. ( Base ` G ) ) -> ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
95 88 90 94 syl2anc 
 |-  ( ph -> ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
96 82 93 95 3eqtrd 
 |-  ( ph -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
97 96 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
98 simpr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) )
99 1 symgid 
 |-  ( D e. V -> ( _I |` D ) = ( 0g ` G ) )
100 3 99 syl 
 |-  ( ph -> ( _I |` D ) = ( 0g ` G ) )
101 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
102 101 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
103 100 102 eqtr4di 
 |-  ( ph -> ( _I |` D ) = ( G gsum (/) ) )
104 103 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( _I |` D ) = ( G gsum (/) ) )
105 97 98 104 3eqtrd 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( G gsum (/) ) )
106 61 65 70 71 72 75 77 105 gsumspl 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) ) = ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) )
107 5 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum W ) = ( _I |` D ) )
108 60 106 107 3eqtr3d 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) )
109 fveqeq2 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( ( # ` x ) = ( L - 2 ) <-> ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) ) )
110 oveq2 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( G gsum x ) = ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) )
111 110 eqeq1d 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( ( G gsum x ) = ( _I |` D ) <-> ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) ) )
112 109 111 anbi12d 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) <-> ( ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) /\ ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) ) ) )
113 112 rspcev 
 |-  ( ( ( W splice <. I , ( I + 2 ) , (/) >. ) e. Word T /\ ( ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) /\ ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) ) ) -> E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
114 14 56 108 113 syl12anc 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
115 10 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
116 114 115 pm2.21dd 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )
117 116 ex 
 |-  ( ph -> ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) ) )
118 4 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> W e. Word T )
119 simprl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> r e. T )
120 simprr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> s e. T )
121 119 120 s2cld 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> <" r s "> e. Word T )
122 splcl 
 |-  ( ( W e. Word T /\ <" r s "> e. Word T ) -> ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T )
123 118 121 122 syl2anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T )
124 123 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T )
125 64 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> G e. Mnd )
126 69 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> W e. Word ( Base ` G ) )
127 26 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> I e. ( 0 ... ( I + 2 ) ) )
128 37 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
129 68 121 sselid 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> <" r s "> e. Word ( Base ` G ) )
130 129 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> <" r s "> e. Word ( Base ` G ) )
131 74 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
132 simprr1 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) )
133 96 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
134 64 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> G e. Mnd )
135 66 a1i 
 |-  ( ph -> T C_ ( Base ` G ) )
136 135 sselda 
 |-  ( ( ph /\ r e. T ) -> r e. ( Base ` G ) )
137 136 adantrr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> r e. ( Base ` G ) )
138 135 sselda 
 |-  ( ( ph /\ s e. T ) -> s e. ( Base ` G ) )
139 138 adantrl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> s e. ( Base ` G ) )
140 61 91 gsumws2 
 |-  ( ( G e. Mnd /\ r e. ( Base ` G ) /\ s e. ( Base ` G ) ) -> ( G gsum <" r s "> ) = ( r ( +g ` G ) s ) )
141 134 137 139 140 syl3anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( G gsum <" r s "> ) = ( r ( +g ` G ) s ) )
142 1 61 91 symgov 
 |-  ( ( r e. ( Base ` G ) /\ s e. ( Base ` G ) ) -> ( r ( +g ` G ) s ) = ( r o. s ) )
143 137 139 142 syl2anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( r ( +g ` G ) s ) = ( r o. s ) )
144 141 143 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( G gsum <" r s "> ) = ( r o. s ) )
145 144 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum <" r s "> ) = ( r o. s ) )
146 132 133 145 3eqtr4rd 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum <" r s "> ) = ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) )
147 61 125 126 127 128 130 131 146 gsumspl 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( G gsum ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) ) )
148 59 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , ( W substr <. I , ( I + 2 ) >. ) >. ) ) = ( G gsum W ) )
149 5 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum W ) = ( _I |` D ) )
150 147 148 149 3eqtrd 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) )
151 26 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> I e. ( 0 ... ( I + 2 ) ) )
152 37 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
153 118 151 152 121 spllen 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) )
154 s2len 
 |-  ( # ` <" r s "> ) = 2
155 154 oveq1i 
 |-  ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) = ( 2 - ( ( I + 2 ) - I ) )
156 46 oveq2d 
 |-  ( ph -> ( 2 - ( ( I + 2 ) - I ) ) = ( 2 - 2 ) )
157 44 subidi 
 |-  ( 2 - 2 ) = 0
158 156 157 eqtrdi 
 |-  ( ph -> ( 2 - ( ( I + 2 ) - I ) ) = 0 )
159 155 158 eqtrid 
 |-  ( ph -> ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) = 0 )
160 159 oveq2d 
 |-  ( ph -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = ( ( # ` W ) + 0 ) )
161 6 52 eqeltrd 
 |-  ( ph -> ( # ` W ) e. CC )
162 161 addid1d 
 |-  ( ph -> ( ( # ` W ) + 0 ) = ( # ` W ) )
163 160 162 6 3eqtrd 
 |-  ( ph -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = L )
164 163 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = L )
165 153 164 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L )
166 165 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L )
167 150 166 jca 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) /\ ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) )
168 27 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( I + 1 ) e. ( 0 ..^ L ) )
169 simprr2 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> A e. dom ( s \ _I ) )
170 1nn0 
 |-  1 e. NN0
171 2nn 
 |-  2 e. NN
172 1lt2 
 |-  1 < 2
173 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
174 170 171 172 173 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
175 154 oveq2i 
 |-  ( 0 ..^ ( # ` <" r s "> ) ) = ( 0 ..^ 2 )
176 174 175 eleqtrri 
 |-  1 e. ( 0 ..^ ( # ` <" r s "> ) )
177 176 a1i 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> 1 e. ( 0 ..^ ( # ` <" r s "> ) ) )
178 118 151 152 121 177 splfv2a 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) = ( <" r s "> ` 1 ) )
179 s2fv1 
 |-  ( s e. T -> ( <" r s "> ` 1 ) = s )
180 179 ad2antll 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( <" r s "> ` 1 ) = s )
181 178 180 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) = s )
182 181 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) = s )
183 182 difeq1d 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) = ( s \ _I ) )
184 183 dmeqd 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) = dom ( s \ _I ) )
185 169 184 eleqtrrd 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) )
186 fzosplitsni 
 |-  ( I e. ( ZZ>= ` 0 ) -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
187 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
188 186 187 eleq2s 
 |-  ( I e. NN0 -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
189 18 188 syl 
 |-  ( ph -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
190 189 adantr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
191 fveq2 
 |-  ( k = j -> ( W ` k ) = ( W ` j ) )
192 191 difeq1d 
 |-  ( k = j -> ( ( W ` k ) \ _I ) = ( ( W ` j ) \ _I ) )
193 192 dmeqd 
 |-  ( k = j -> dom ( ( W ` k ) \ _I ) = dom ( ( W ` j ) \ _I ) )
194 193 eleq2d 
 |-  ( k = j -> ( A e. dom ( ( W ` k ) \ _I ) <-> A e. dom ( ( W ` j ) \ _I ) ) )
195 194 notbid 
 |-  ( k = j -> ( -. A e. dom ( ( W ` k ) \ _I ) <-> -. A e. dom ( ( W ` j ) \ _I ) ) )
196 195 rspccva 
 |-  ( ( A. k e. ( 0 ..^ I ) -. A e. dom ( ( W ` k ) \ _I ) /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
197 9 196 sylan 
 |-  ( ( ph /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
198 197 adantlr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
199 4 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> W e. Word T )
200 26 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> I e. ( 0 ... ( I + 2 ) ) )
201 37 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
202 121 adantr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> <" r s "> e. Word T )
203 simpr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> j e. ( 0 ..^ I ) )
204 199 200 201 202 203 splfv1 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) = ( W ` j ) )
205 204 difeq1d 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = ( ( W ` j ) \ _I ) )
206 205 dmeqd 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = dom ( ( W ` j ) \ _I ) )
207 198 206 neleqtrrd 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
208 207 ex 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( j e. ( 0 ..^ I ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
209 208 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( j e. ( 0 ..^ I ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
210 simprr3 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> -. A e. dom ( r \ _I ) )
211 0nn0 
 |-  0 e. NN0
212 2pos 
 |-  0 < 2
213 elfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> ( 0 e. NN0 /\ 2 e. NN /\ 0 < 2 ) )
214 211 171 212 213 mpbir3an 
 |-  0 e. ( 0 ..^ 2 )
215 214 175 eleqtrri 
 |-  0 e. ( 0 ..^ ( # ` <" r s "> ) )
216 215 a1i 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> 0 e. ( 0 ..^ ( # ` <" r s "> ) ) )
217 118 151 152 121 216 splfv2a 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 0 ) ) = ( <" r s "> ` 0 ) )
218 32 addid1d 
 |-  ( ph -> ( I + 0 ) = I )
219 218 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( I + 0 ) = I )
220 219 fveq2d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 0 ) ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) )
221 s2fv0 
 |-  ( r e. T -> ( <" r s "> ` 0 ) = r )
222 221 ad2antrl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( <" r s "> ` 0 ) = r )
223 217 220 222 3eqtr3d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) = r )
224 223 difeq1d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) = ( r \ _I ) )
225 224 dmeqd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) = dom ( r \ _I ) )
226 225 eleq2d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) <-> A e. dom ( r \ _I ) ) )
227 226 adantrr 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) <-> A e. dom ( r \ _I ) ) )
228 210 227 mtbird 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) )
229 fveq2 
 |-  ( j = I -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) )
230 229 difeq1d 
 |-  ( j = I -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) )
231 230 dmeqd 
 |-  ( j = I -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) )
232 231 eleq2d 
 |-  ( j = I -> ( A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) <-> A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) ) )
233 232 notbid 
 |-  ( j = I -> ( -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) <-> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) ) )
234 228 233 syl5ibrcom 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( j = I -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
235 209 234 jaod 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( j e. ( 0 ..^ I ) \/ j = I ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
236 190 235 sylbid 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( j e. ( 0 ..^ ( I + 1 ) ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
237 236 ralrimiv 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
238 168 185 237 3jca 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
239 oveq2 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( G gsum w ) = ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) )
240 239 eqeq1d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( G gsum w ) = ( _I |` D ) <-> ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) ) )
241 fveqeq2 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( # ` w ) = L <-> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) )
242 240 241 anbi12d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) <-> ( ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) /\ ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) ) )
243 fveq1 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( w ` ( I + 1 ) ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) )
244 243 difeq1d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( w ` ( I + 1 ) ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) )
245 244 dmeqd 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> dom ( ( w ` ( I + 1 ) ) \ _I ) = dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) )
246 245 eleq2d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( A e. dom ( ( w ` ( I + 1 ) ) \ _I ) <-> A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) ) )
247 fveq1 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( w ` j ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) )
248 247 difeq1d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( w ` j ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
249 248 dmeqd 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> dom ( ( w ` j ) \ _I ) = dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
250 249 eleq2d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( A e. dom ( ( w ` j ) \ _I ) <-> A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
251 250 notbid 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( -. A e. dom ( ( w ` j ) \ _I ) <-> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
252 251 ralbidv 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) <-> A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
253 246 252 3anbi23d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) <-> ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) ) )
254 242 253 anbi12d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) <-> ( ( ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) /\ ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) ) ) )
255 254 rspcev 
 |-  ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T /\ ( ( ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( _I |` D ) /\ ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )
256 124 167 238 255 syl12anc 
 |-  ( ( ph /\ ( ( r e. T /\ s e. T ) /\ ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )
257 256 expr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) ) )
258 257 rexlimdvva 
 |-  ( ph -> ( E. r e. T E. s e. T ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) ) )
259 2 3 87 89 8 psgnunilem1 
 |-  ( ph -> ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) \/ E. r e. T E. s e. T ( ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( r o. s ) /\ A e. dom ( s \ _I ) /\ -. A e. dom ( r \ _I ) ) ) )
260 117 258 259 mpjaod 
 |-  ( ph -> E. w e. Word T ( ( ( G gsum w ) = ( _I |` D ) /\ ( # ` w ) = L ) /\ ( ( I + 1 ) e. ( 0 ..^ L ) /\ A e. dom ( ( w ` ( I + 1 ) ) \ _I ) /\ A. j e. ( 0 ..^ ( I + 1 ) ) -. A e. dom ( ( w ` j ) \ _I ) ) ) )