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 sseldi 
 |-  ( 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 syl5eq 
 |-  ( 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 grpmnd 
 |-  ( G e. Grp -> G e. Mnd )
65 63 64 syl 
 |-  ( ph -> G e. Mnd )
66 65 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> G e. Mnd )
67 2 1 61 symgtrf 
 |-  T C_ ( Base ` G )
68 sswrd 
 |-  ( T C_ ( Base ` G ) -> Word T C_ Word ( Base ` G ) )
69 67 68 ax-mp 
 |-  Word T C_ Word ( Base ` G )
70 69 4 sseldi 
 |-  ( ph -> W e. Word ( Base ` G ) )
71 70 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> W e. Word ( Base ` G ) )
72 26 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> I e. ( 0 ... ( I + 2 ) ) )
73 37 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
74 swrdcl 
 |-  ( W e. Word ( Base ` G ) -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
75 70 74 syl 
 |-  ( ph -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
76 75 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( W substr <. I , ( I + 2 ) >. ) e. Word ( Base ` G ) )
77 wrd0 
 |-  (/) e. Word ( Base ` G )
78 77 a1i 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> (/) e. Word ( Base ` G ) )
79 6 oveq2d 
 |-  ( ph -> ( 0 ..^ ( # ` W ) ) = ( 0 ..^ L ) )
80 27 79 eleqtrrd 
 |-  ( ph -> ( I + 1 ) e. ( 0 ..^ ( # ` W ) ) )
81 swrds2 
 |-  ( ( W e. Word T /\ I e. NN0 /\ ( I + 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
82 4 18 80 81 syl3anc 
 |-  ( ph -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
83 82 oveq2d 
 |-  ( ph -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( G gsum <" ( W ` I ) ( W ` ( I + 1 ) ) "> ) )
84 wrdf 
 |-  ( W e. Word T -> W : ( 0 ..^ ( # ` W ) ) --> T )
85 4 84 syl 
 |-  ( ph -> W : ( 0 ..^ ( # ` W ) ) --> T )
86 79 feq2d 
 |-  ( ph -> ( W : ( 0 ..^ ( # ` W ) ) --> T <-> W : ( 0 ..^ L ) --> T ) )
87 85 86 mpbid 
 |-  ( ph -> W : ( 0 ..^ L ) --> T )
88 87 7 ffvelrnd 
 |-  ( ph -> ( W ` I ) e. T )
89 67 88 sseldi 
 |-  ( ph -> ( W ` I ) e. ( Base ` G ) )
90 87 27 ffvelrnd 
 |-  ( ph -> ( W ` ( I + 1 ) ) e. T )
91 67 90 sseldi 
 |-  ( ph -> ( W ` ( I + 1 ) ) e. ( Base ` G ) )
92 eqid 
 |-  ( +g ` G ) = ( +g ` G )
93 61 92 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 ) ) ) )
94 65 89 91 93 syl3anc 
 |-  ( ph -> ( G gsum <" ( W ` I ) ( W ` ( I + 1 ) ) "> ) = ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) )
95 1 61 92 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 ) ) ) )
96 89 91 95 syl2anc 
 |-  ( ph -> ( ( W ` I ) ( +g ` G ) ( W ` ( I + 1 ) ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
97 83 94 96 3eqtrd 
 |-  ( ph -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
98 97 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) )
99 simpr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) )
100 1 symgid 
 |-  ( D e. V -> ( _I |` D ) = ( 0g ` G ) )
101 3 100 syl 
 |-  ( ph -> ( _I |` D ) = ( 0g ` G ) )
102 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
103 102 gsum0 
 |-  ( G gsum (/) ) = ( 0g ` G )
104 101 103 eqtr4di 
 |-  ( ph -> ( _I |` D ) = ( G gsum (/) ) )
105 104 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( _I |` D ) = ( G gsum (/) ) )
106 98 99 105 3eqtrd 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W substr <. I , ( I + 2 ) >. ) ) = ( G gsum (/) ) )
107 61 66 71 72 73 76 78 106 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 ) , (/) >. ) ) )
108 5 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum W ) = ( _I |` D ) )
109 60 107 108 3eqtr3d 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) )
110 fveqeq2 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( ( # ` x ) = ( L - 2 ) <-> ( # ` ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( L - 2 ) ) )
111 oveq2 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( G gsum x ) = ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) )
112 111 eqeq1d 
 |-  ( x = ( W splice <. I , ( I + 2 ) , (/) >. ) -> ( ( G gsum x ) = ( _I |` D ) <-> ( G gsum ( W splice <. I , ( I + 2 ) , (/) >. ) ) = ( _I |` D ) ) )
113 110 112 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 ) ) ) )
114 113 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 ) ) )
115 14 56 109 114 syl12anc 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
116 10 adantr 
 |-  ( ( ph /\ ( ( W ` I ) o. ( W ` ( I + 1 ) ) ) = ( _I |` D ) ) -> -. E. x e. Word T ( ( # ` x ) = ( L - 2 ) /\ ( G gsum x ) = ( _I |` D ) ) )
117 115 116 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 ) ) ) )
118 117 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 ) ) ) ) )
119 4 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> W e. Word T )
120 simprl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> r e. T )
121 simprr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> s e. T )
122 120 121 s2cld 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> <" r s "> e. Word T )
123 splcl 
 |-  ( ( W e. Word T /\ <" r s "> e. Word T ) -> ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T )
124 119 122 123 syl2anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( W splice <. I , ( I + 2 ) , <" r s "> >. ) e. Word T )
125 124 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 )
126 65 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 )
127 70 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 ) )
128 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 ) ) )
129 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 ) ) )
130 69 122 sseldi 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> <" r s "> e. Word ( Base ` G ) )
131 130 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 ) )
132 75 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 ) )
133 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 ) )
134 97 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 ) ) ) )
135 65 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> G e. Mnd )
136 67 a1i 
 |-  ( ph -> T C_ ( Base ` G ) )
137 136 sselda 
 |-  ( ( ph /\ r e. T ) -> r e. ( Base ` G ) )
138 137 adantrr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> r e. ( Base ` G ) )
139 136 sselda 
 |-  ( ( ph /\ s e. T ) -> s e. ( Base ` G ) )
140 139 adantrl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> s e. ( Base ` G ) )
141 61 92 gsumws2 
 |-  ( ( G e. Mnd /\ r e. ( Base ` G ) /\ s e. ( Base ` G ) ) -> ( G gsum <" r s "> ) = ( r ( +g ` G ) s ) )
142 135 138 140 141 syl3anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( G gsum <" r s "> ) = ( r ( +g ` G ) s ) )
143 1 61 92 symgov 
 |-  ( ( r e. ( Base ` G ) /\ s e. ( Base ` G ) ) -> ( r ( +g ` G ) s ) = ( r o. s ) )
144 138 140 143 syl2anc 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( r ( +g ` G ) s ) = ( r o. s ) )
145 142 144 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( G gsum <" r s "> ) = ( r o. s ) )
146 145 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 ) )
147 133 134 146 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 ) >. ) ) )
148 61 126 127 128 129 131 132 147 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 ) >. ) >. ) ) )
149 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 ) )
150 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 ) )
151 148 149 150 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 ) )
152 26 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> I e. ( 0 ... ( I + 2 ) ) )
153 37 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
154 119 152 153 122 spllen 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) )
155 s2len 
 |-  ( # ` <" r s "> ) = 2
156 155 oveq1i 
 |-  ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) = ( 2 - ( ( I + 2 ) - I ) )
157 46 oveq2d 
 |-  ( ph -> ( 2 - ( ( I + 2 ) - I ) ) = ( 2 - 2 ) )
158 44 subidi 
 |-  ( 2 - 2 ) = 0
159 157 158 eqtrdi 
 |-  ( ph -> ( 2 - ( ( I + 2 ) - I ) ) = 0 )
160 156 159 syl5eq 
 |-  ( ph -> ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) = 0 )
161 160 oveq2d 
 |-  ( ph -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = ( ( # ` W ) + 0 ) )
162 6 52 eqeltrd 
 |-  ( ph -> ( # ` W ) e. CC )
163 162 addid1d 
 |-  ( ph -> ( ( # ` W ) + 0 ) = ( # ` W ) )
164 161 163 6 3eqtrd 
 |-  ( ph -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = L )
165 164 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( # ` W ) + ( ( # ` <" r s "> ) - ( ( I + 2 ) - I ) ) ) = L )
166 154 165 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L )
167 166 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 )
168 151 167 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 ) )
169 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 ) )
170 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 ) )
171 1nn0 
 |-  1 e. NN0
172 2nn 
 |-  2 e. NN
173 1lt2 
 |-  1 < 2
174 elfzo0 
 |-  ( 1 e. ( 0 ..^ 2 ) <-> ( 1 e. NN0 /\ 2 e. NN /\ 1 < 2 ) )
175 171 172 173 174 mpbir3an 
 |-  1 e. ( 0 ..^ 2 )
176 155 oveq2i 
 |-  ( 0 ..^ ( # ` <" r s "> ) ) = ( 0 ..^ 2 )
177 175 176 eleqtrri 
 |-  1 e. ( 0 ..^ ( # ` <" r s "> ) )
178 177 a1i 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> 1 e. ( 0 ..^ ( # ` <" r s "> ) ) )
179 119 152 153 122 178 splfv2a 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) = ( <" r s "> ` 1 ) )
180 s2fv1 
 |-  ( s e. T -> ( <" r s "> ` 1 ) = s )
181 180 ad2antll 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( <" r s "> ` 1 ) = s )
182 179 181 eqtrd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) = s )
183 182 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 )
184 183 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 ) )
185 184 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 ) )
186 170 185 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 ) )
187 fzosplitsni 
 |-  ( I e. ( ZZ>= ` 0 ) -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
188 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
189 187 188 eleq2s 
 |-  ( I e. NN0 -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
190 18 189 syl 
 |-  ( ph -> ( j e. ( 0 ..^ ( I + 1 ) ) <-> ( j e. ( 0 ..^ I ) \/ j = I ) ) )
191 190 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 ) ) )
192 fveq2 
 |-  ( k = j -> ( W ` k ) = ( W ` j ) )
193 192 difeq1d 
 |-  ( k = j -> ( ( W ` k ) \ _I ) = ( ( W ` j ) \ _I ) )
194 193 dmeqd 
 |-  ( k = j -> dom ( ( W ` k ) \ _I ) = dom ( ( W ` j ) \ _I ) )
195 194 eleq2d 
 |-  ( k = j -> ( A e. dom ( ( W ` k ) \ _I ) <-> A e. dom ( ( W ` j ) \ _I ) ) )
196 195 notbid 
 |-  ( k = j -> ( -. A e. dom ( ( W ` k ) \ _I ) <-> -. A e. dom ( ( W ` j ) \ _I ) ) )
197 196 rspccva 
 |-  ( ( A. k e. ( 0 ..^ I ) -. A e. dom ( ( W ` k ) \ _I ) /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
198 9 197 sylan 
 |-  ( ( ph /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
199 198 adantlr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> -. A e. dom ( ( W ` j ) \ _I ) )
200 4 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> W e. Word T )
201 26 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> I e. ( 0 ... ( I + 2 ) ) )
202 37 ad2antrr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( I + 2 ) e. ( 0 ... ( # ` W ) ) )
203 122 adantr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> <" r s "> e. Word T )
204 simpr 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> j e. ( 0 ..^ I ) )
205 200 201 202 203 204 splfv1 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) = ( W ` j ) )
206 205 difeq1d 
 |-  ( ( ( ph /\ ( r e. T /\ s e. T ) ) /\ j e. ( 0 ..^ I ) ) -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = ( ( W ` j ) \ _I ) )
207 206 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 ) )
208 199 207 neleqtrrd 
 |-  ( ( ( 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 ex 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( j e. ( 0 ..^ I ) -> -. A e. dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) ) )
210 209 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 ) ) )
211 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 ) )
212 0nn0 
 |-  0 e. NN0
213 2pos 
 |-  0 < 2
214 elfzo0 
 |-  ( 0 e. ( 0 ..^ 2 ) <-> ( 0 e. NN0 /\ 2 e. NN /\ 0 < 2 ) )
215 212 172 213 214 mpbir3an 
 |-  0 e. ( 0 ..^ 2 )
216 215 176 eleqtrri 
 |-  0 e. ( 0 ..^ ( # ` <" r s "> ) )
217 216 a1i 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> 0 e. ( 0 ..^ ( # ` <" r s "> ) ) )
218 119 152 153 122 217 splfv2a 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 0 ) ) = ( <" r s "> ` 0 ) )
219 32 addid1d 
 |-  ( ph -> ( I + 0 ) = I )
220 219 adantr 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( I + 0 ) = I )
221 220 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 ) )
222 s2fv0 
 |-  ( r e. T -> ( <" r s "> ` 0 ) = r )
223 222 ad2antrl 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( <" r s "> ` 0 ) = r )
224 218 221 223 3eqtr3d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) = r )
225 224 difeq1d 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) = ( r \ _I ) )
226 225 dmeqd 
 |-  ( ( ph /\ ( r e. T /\ s e. T ) ) -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) = dom ( r \ _I ) )
227 226 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 ) ) )
228 227 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 ) ) )
229 211 228 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 ) )
230 fveq2 
 |-  ( j = I -> ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) )
231 230 difeq1d 
 |-  ( j = I -> ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) )
232 231 dmeqd 
 |-  ( j = I -> dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) = dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` I ) \ _I ) )
233 232 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 ) ) )
234 233 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 ) ) )
235 229 234 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 ) ) )
236 210 235 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 ) ) )
237 191 236 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 ) ) )
238 237 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 ) )
239 169 186 238 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 ) ) )
240 oveq2 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( G gsum w ) = ( G gsum ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) )
241 240 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 ) ) )
242 fveqeq2 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( # ` w ) = L <-> ( # ` ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ) = L ) )
243 241 242 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 ) ) )
244 fveq1 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( w ` ( I + 1 ) ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) )
245 244 difeq1d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( w ` ( I + 1 ) ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` ( I + 1 ) ) \ _I ) )
246 245 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 ) )
247 246 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 ) ) )
248 fveq1 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( w ` j ) = ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) )
249 248 difeq1d 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> ( ( w ` j ) \ _I ) = ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
250 249 dmeqd 
 |-  ( w = ( W splice <. I , ( I + 2 ) , <" r s "> >. ) -> dom ( ( w ` j ) \ _I ) = dom ( ( ( W splice <. I , ( I + 2 ) , <" r s "> >. ) ` j ) \ _I ) )
251 250 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 ) ) )
252 251 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 ) ) )
253 252 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 ) ) )
254 247 253 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 ) ) ) )
255 243 254 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 ) ) ) ) )
256 255 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 ) ) ) )
257 125 168 239 256 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 ) ) ) )
258 257 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 ) ) ) ) )
259 258 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 ) ) ) ) )
260 2 3 88 90 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 ) ) ) )
261 118 259 260 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 ) ) ) )