MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgredleme Unicode version

Theorem efgredleme 15068
Description: Lemma for efgred 15073. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w  |-  W  =  (  _I  ` Word  ( I  X.  2o ) )
efgval.r  |-  .~  =  ( ~FG  `  I )
efgval2.m  |-  M  =  ( y  e.  I ,  z  e.  2o  |->  <. y ,  ( 1o 
\  z ) >.
)
efgval2.t  |-  T  =  ( v  e.  W  |->  ( n  e.  ( 0 ... ( # `  v ) ) ,  w  e.  ( I  X.  2o )  |->  ( v splice  <. n ,  n ,  <" w ( M `  w ) "> >. )
) )
efgred.d  |-  D  =  ( W  \  U_ x  e.  W  ran  ( T `  x ) )
efgred.s  |-  S  =  ( m  e.  {
t  e.  (Word  W  \  { (/) } )  |  ( ( t ` 
0 )  e.  D  /\  A. k  e.  ( 1..^ ( # `  t
) ) ( t `
 k )  e. 
ran  ( T `  ( t `  (
k  -  1 ) ) ) ) } 
|->  ( m `  (
( # `  m )  -  1 ) ) )
efgredlem.1  |-  ( ph  ->  A. a  e.  dom  S A. b  e.  dom  S ( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  ->  ( ( S `  a )  =  ( S `  b )  ->  (
a `  0 )  =  ( b ` 
0 ) ) ) )
efgredlem.2  |-  ( ph  ->  A  e.  dom  S
)
efgredlem.3  |-  ( ph  ->  B  e.  dom  S
)
efgredlem.4  |-  ( ph  ->  ( S `  A
)  =  ( S `
 B ) )
efgredlem.5  |-  ( ph  ->  -.  ( A ` 
0 )  =  ( B `  0 ) )
efgredlemb.k  |-  K  =  ( ( ( # `  A )  -  1 )  -  1 )
efgredlemb.l  |-  L  =  ( ( ( # `  B )  -  1 )  -  1 )
efgredlemb.p  |-  ( ph  ->  P  e.  ( 0 ... ( # `  ( A `  K )
) ) )
efgredlemb.q  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( B `  L )
) ) )
efgredlemb.u  |-  ( ph  ->  U  e.  ( I  X.  2o ) )
efgredlemb.v  |-  ( ph  ->  V  e.  ( I  X.  2o ) )
efgredlemb.6  |-  ( ph  ->  ( S `  A
)  =  ( P ( T `  ( A `  K )
) U ) )
efgredlemb.7  |-  ( ph  ->  ( S `  B
)  =  ( Q ( T `  ( B `  L )
) V ) )
efgredlemb.8  |-  ( ph  ->  -.  ( A `  K )  =  ( B `  L ) )
efgredlemd.9  |-  ( ph  ->  P  e.  ( ZZ>= `  ( Q  +  2
) ) )
efgredlemd.c  |-  ( ph  ->  C  e.  dom  S
)
efgredlemd.sc  |-  ( ph  ->  ( S `  C
)  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
Assertion
Ref Expression
efgredleme  |-  ( ph  ->  ( ( A `  K )  e.  ran  ( T `  ( S `
 C ) )  /\  ( B `  L )  e.  ran  ( T `  ( S `
 C ) ) ) )
Distinct variable groups:    a, b, A    y, a, z, b    L, a, b    K, a, b    t, n, v, w, y, z, P   
m, a, n, t, v, w, x, M, b    U, n, v, w, y, z    k, a, T, b, m, t, x    n, V, v, w, y, z    Q, n, t, v, w, y, z    W, a, b    k, n, v, w, y, z, W, m, t, x    .~ , a, b, m, t, x, y, z    B, a, b    C, a, b, k, m, n, t, v, w, x, y, z    S, a, b    I,
a, b, m, n, t, v, w, x, y, z    D, a, b, m, t
Allowed substitution hints:    ph( x, y, z, w, v, t, k, m, n, a, b)    A( x, y, z, w, v, t, k, m, n)    B( x, y, z, w, v, t, k, m, n)    D( x, y, z, w, v, k, n)    P( x, k, m, a, b)    Q( x, k, m, a, b)    .~ ( w, v, k, n)    S( x, y, z, w, v, t, k, m, n)    T( y, z, w, v, n)    U( x, t, k, m, a, b)    I( k)    K( x, y, z, w, v, t, k, m, n)    L( x, y, z, w, v, t, k, m, n)    M( y, z, k)    V( x, t, k, m, a, b)

Proof of Theorem efgredleme
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 efgredlemd.c . . . . . 6  |-  ( ph  ->  C  e.  dom  S
)
2 efgval.w . . . . . . . . 9  |-  W  =  (  _I  ` Word  ( I  X.  2o ) )
3 efgval.r . . . . . . . . 9  |-  .~  =  ( ~FG  `  I )
4 efgval2.m . . . . . . . . 9  |-  M  =  ( y  e.  I ,  z  e.  2o  |->  <. y ,  ( 1o 
\  z ) >.
)
5 efgval2.t . . . . . . . . 9  |-  T  =  ( v  e.  W  |->  ( n  e.  ( 0 ... ( # `  v ) ) ,  w  e.  ( I  X.  2o )  |->  ( v splice  <. n ,  n ,  <" w ( M `  w ) "> >. )
) )
6 efgred.d . . . . . . . . 9  |-  D  =  ( W  \  U_ x  e.  W  ran  ( T `  x ) )
7 efgred.s . . . . . . . . 9  |-  S  =  ( m  e.  {
t  e.  (Word  W  \  { (/) } )  |  ( ( t ` 
0 )  e.  D  /\  A. k  e.  ( 1..^ ( # `  t
) ) ( t `
 k )  e. 
ran  ( T `  ( t `  (
k  -  1 ) ) ) ) } 
|->  ( m `  (
( # `  m )  -  1 ) ) )
82, 3, 4, 5, 6, 7efgsf 15054 . . . . . . . 8  |-  S : { t  e.  (Word 
W  \  { (/) } )  |  ( ( t `
 0 )  e.  D  /\  A. k  e.  ( 1..^ ( # `  t ) ) ( t `  k )  e.  ran  ( T `
 ( t `  ( k  -  1 ) ) ) ) } --> W
98fdmi 5410 . . . . . . . . 9  |-  dom  S  =  { t  e.  (Word 
W  \  { (/) } )  |  ( ( t `
 0 )  e.  D  /\  A. k  e.  ( 1..^ ( # `  t ) ) ( t `  k )  e.  ran  ( T `
 ( t `  ( k  -  1 ) ) ) ) }
109feq2i 5400 . . . . . . . 8  |-  ( S : dom  S --> W  <->  S : { t  e.  (Word 
W  \  { (/) } )  |  ( ( t `
 0 )  e.  D  /\  A. k  e.  ( 1..^ ( # `  t ) ) ( t `  k )  e.  ran  ( T `
 ( t `  ( k  -  1 ) ) ) ) } --> W )
118, 10mpbir 200 . . . . . . 7  |-  S : dom  S --> W
1211ffvelrni 5680 . . . . . 6  |-  ( C  e.  dom  S  -> 
( S `  C
)  e.  W )
131, 12syl 15 . . . . 5  |-  ( ph  ->  ( S `  C
)  e.  W )
14 efgredlemb.q . . . . . . 7  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( B `  L )
) ) )
15 elfzuz 10810 . . . . . . 7  |-  ( Q  e.  ( 0 ... ( # `  ( B `  L )
) )  ->  Q  e.  ( ZZ>= `  0 )
)
1614, 15syl 15 . . . . . 6  |-  ( ph  ->  Q  e.  ( ZZ>= ` 
0 ) )
17 efgredlemd.sc . . . . . . . . . 10  |-  ( ph  ->  ( S `  C
)  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
1817fveq2d 5545 . . . . . . . . 9  |-  ( ph  ->  ( # `  ( S `  C )
)  =  ( # `  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) ) )
19 fviss 5596 . . . . . . . . . . . . 13  |-  (  _I 
` Word  ( I  X.  2o ) )  C_ Word  ( I  X.  2o )
202, 19eqsstri 3221 . . . . . . . . . . . 12  |-  W  C_ Word  ( I  X.  2o )
21 efgredlem.1 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. a  e.  dom  S A. b  e.  dom  S ( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  ->  ( ( S `  a )  =  ( S `  b )  ->  (
a `  0 )  =  ( b ` 
0 ) ) ) )
22 efgredlem.2 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  e.  dom  S
)
23 efgredlem.3 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  dom  S
)
24 efgredlem.4 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( S `  A
)  =  ( S `
 B ) )
25 efgredlem.5 . . . . . . . . . . . . . 14  |-  ( ph  ->  -.  ( A ` 
0 )  =  ( B `  0 ) )
26 efgredlemb.k . . . . . . . . . . . . . 14  |-  K  =  ( ( ( # `  A )  -  1 )  -  1 )
27 efgredlemb.l . . . . . . . . . . . . . 14  |-  L  =  ( ( ( # `  B )  -  1 )  -  1 )
282, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27efgredlemf 15066 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  K )  e.  W  /\  ( B `  L
)  e.  W ) )
2928simprd 449 . . . . . . . . . . . 12  |-  ( ph  ->  ( B `  L
)  e.  W )
3020, 29sseldi 3191 . . . . . . . . . . 11  |-  ( ph  ->  ( B `  L
)  e. Word  ( I  X.  2o ) )
31 swrdcl 11468 . . . . . . . . . . 11  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o ) )
3230, 31syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o ) )
3328simpld 445 . . . . . . . . . . . 12  |-  ( ph  ->  ( A `  K
)  e.  W )
3420, 33sseldi 3191 . . . . . . . . . . 11  |-  ( ph  ->  ( A `  K
)  e. Word  ( I  X.  2o ) )
35 swrdcl 11468 . . . . . . . . . . 11  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )  e. Word  ( I  X.  2o ) )
3634, 35syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )
37 ccatlen 11446 . . . . . . . . . 10  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )  ->  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) )  =  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) ) )
3832, 36, 37syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) )  =  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) ) )
39 swrd0len 11471 . . . . . . . . . . . 12  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  Q  e.  ( 0 ... ( # `
 ( B `  L ) ) ) )  ->  ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  =  Q )
4030, 14, 39syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  =  Q )
41 2nn0 9998 . . . . . . . . . . . . . 14  |-  2  e.  NN0
42 uzaddcl 10291 . . . . . . . . . . . . . 14  |-  ( ( Q  e.  ( ZZ>= ` 
0 )  /\  2  e.  NN0 )  ->  ( Q  +  2 )  e.  ( ZZ>= `  0
) )
4316, 41, 42sylancl 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  +  2 )  e.  ( ZZ>= ` 
0 ) )
44 efgredlemb.p . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  ( 0 ... ( # `  ( A `  K )
) ) )
45 elfzuz3 10811 . . . . . . . . . . . . . . 15  |-  ( P  e.  ( 0 ... ( # `  ( A `  K )
) )  ->  ( # `
 ( A `  K ) )  e.  ( ZZ>= `  P )
)
4644, 45syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  P ) )
47 efgredlemd.9 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  ( ZZ>= `  ( Q  +  2
) ) )
48 uztrn 10260 . . . . . . . . . . . . . 14  |-  ( ( ( # `  ( A `  K )
)  e.  ( ZZ>= `  P )  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  ( Q  +  2
) ) )
4946, 47, 48syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  ( Q  +  2
) ) )
50 elfzuzb 10808 . . . . . . . . . . . . 13  |-  ( ( Q  +  2 )  e.  ( 0 ... ( # `  ( A `  K )
) )  <->  ( ( Q  +  2 )  e.  ( ZZ>= `  0
)  /\  ( # `  ( A `  K )
)  e.  ( ZZ>= `  ( Q  +  2
) ) ) )
5143, 49, 50sylanbrc 645 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  +  2 )  e.  ( 0 ... ( # `  ( A `  K )
) ) )
52 lencl 11437 . . . . . . . . . . . . . . 15  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( # `  ( A `  K
) )  e.  NN0 )
5334, 52syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  NN0 )
54 nn0uz 10278 . . . . . . . . . . . . . 14  |-  NN0  =  ( ZZ>= `  0 )
5553, 54syl6eleq 2386 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= ` 
0 ) )
56 eluzfz2 10820 . . . . . . . . . . . . 13  |-  ( (
# `  ( A `  K ) )  e.  ( ZZ>= `  0 )  ->  ( # `  ( A `  K )
)  e.  ( 0 ... ( # `  ( A `  K )
) ) )
5755, 56syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( 0 ... ( # `  ( A `  K )
) ) )
58 swrdlen 11472 . . . . . . . . . . . 12  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  ( Q  +  2 )  e.  ( 0 ... ( # `  ( A `  K )
) )  /\  ( # `
 ( A `  K ) )  e.  ( 0 ... ( # `
 ( A `  K ) ) ) )  ->  ( # `  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( # `  ( A `  K )
)  -  ( Q  +  2 ) ) )
5934, 51, 57, 58syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( # `  ( A `  K )
)  -  ( Q  +  2 ) ) )
6040, 59oveq12d 5892 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) )  =  ( Q  +  ( (
# `  ( A `  K ) )  -  ( Q  +  2
) ) ) )
61 elfzelz 10814 . . . . . . . . . . . . 13  |-  ( Q  e.  ( 0 ... ( # `  ( B `  L )
) )  ->  Q  e.  ZZ )
6214, 61syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ZZ )
6362zcnd 10134 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  CC )
6453nn0cnd 10036 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  CC )
65 2z 10070 . . . . . . . . . . . . 13  |-  2  e.  ZZ
66 zaddcl 10075 . . . . . . . . . . . . 13  |-  ( ( Q  e.  ZZ  /\  2  e.  ZZ )  ->  ( Q  +  2 )  e.  ZZ )
6762, 65, 66sylancl 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( Q  +  2 )  e.  ZZ )
6867zcnd 10134 . . . . . . . . . . 11  |-  ( ph  ->  ( Q  +  2 )  e.  CC )
6963, 64, 68addsubassd 9193 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  +  ( # `  ( A `
 K ) ) )  -  ( Q  +  2 ) )  =  ( Q  +  ( ( # `  ( A `  K )
)  -  ( Q  +  2 ) ) ) )
70 2cn 9832 . . . . . . . . . . . 12  |-  2  e.  CC
7170a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  CC )
7263, 64, 71pnpcand 9210 . . . . . . . . . 10  |-  ( ph  ->  ( ( Q  +  ( # `  ( A `
 K ) ) )  -  ( Q  +  2 ) )  =  ( ( # `  ( A `  K
) )  -  2 ) )
7360, 69, 723eqtr2d 2334 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) )  =  ( ( # `  ( A `  K )
)  -  2 ) )
7418, 38, 733eqtrd 2332 . . . . . . . 8  |-  ( ph  ->  ( # `  ( S `  C )
)  =  ( (
# `  ( A `  K ) )  - 
2 ) )
75 elfzelz 10814 . . . . . . . . . . 11  |-  ( P  e.  ( 0 ... ( # `  ( A `  K )
) )  ->  P  e.  ZZ )
7644, 75syl 15 . . . . . . . . . 10  |-  ( ph  ->  P  e.  ZZ )
77 zsubcl 10077 . . . . . . . . . 10  |-  ( ( P  e.  ZZ  /\  2  e.  ZZ )  ->  ( P  -  2 )  e.  ZZ )
7876, 65, 77sylancl 643 . . . . . . . . 9  |-  ( ph  ->  ( P  -  2 )  e.  ZZ )
7965a1i 10 . . . . . . . . 9  |-  ( ph  ->  2  e.  ZZ )
8076zcnd 10134 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  CC )
81 npcan 9076 . . . . . . . . . . . 12  |-  ( ( P  e.  CC  /\  2  e.  CC )  ->  ( ( P  - 
2 )  +  2 )  =  P )
8280, 70, 81sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( ( P  - 
2 )  +  2 )  =  P )
8382fveq2d 5545 . . . . . . . . . 10  |-  ( ph  ->  ( ZZ>= `  ( ( P  -  2 )  +  2 ) )  =  ( ZZ>= `  P
) )
8446, 83eleqtrrd 2373 . . . . . . . . 9  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  ( ( P  - 
2 )  +  2 ) ) )
85 eluzsub 10273 . . . . . . . . 9  |-  ( ( ( P  -  2 )  e.  ZZ  /\  2  e.  ZZ  /\  ( # `
 ( A `  K ) )  e.  ( ZZ>= `  ( ( P  -  2 )  +  2 ) ) )  ->  ( ( # `
 ( A `  K ) )  - 
2 )  e.  (
ZZ>= `  ( P  - 
2 ) ) )
8678, 79, 84, 85syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( ( # `  ( A `  K )
)  -  2 )  e.  ( ZZ>= `  ( P  -  2 ) ) )
8774, 86eqeltrd 2370 . . . . . . 7  |-  ( ph  ->  ( # `  ( S `  C )
)  e.  ( ZZ>= `  ( P  -  2
) ) )
88 eluzsub 10273 . . . . . . . 8  |-  ( ( Q  e.  ZZ  /\  2  e.  ZZ  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  ->  ( P  -  2 )  e.  ( ZZ>= `  Q )
)
8962, 79, 47, 88syl3anc 1182 . . . . . . 7  |-  ( ph  ->  ( P  -  2 )  e.  ( ZZ>= `  Q ) )
90 uztrn 10260 . . . . . . 7  |-  ( ( ( # `  ( S `  C )
)  e.  ( ZZ>= `  ( P  -  2
) )  /\  ( P  -  2 )  e.  ( ZZ>= `  Q
) )  ->  ( # `
 ( S `  C ) )  e.  ( ZZ>= `  Q )
)
9187, 89, 90syl2anc 642 . . . . . 6  |-  ( ph  ->  ( # `  ( S `  C )
)  e.  ( ZZ>= `  Q ) )
92 elfzuzb 10808 . . . . . 6  |-  ( Q  e.  ( 0 ... ( # `  ( S `  C )
) )  <->  ( Q  e.  ( ZZ>= `  0 )  /\  ( # `  ( S `  C )
)  e.  ( ZZ>= `  Q ) ) )
9316, 91, 92sylanbrc 645 . . . . 5  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( S `  C )
) ) )
94 efgredlemb.v . . . . 5  |-  ( ph  ->  V  e.  ( I  X.  2o ) )
952, 3, 4, 5efgtval 15048 . . . . 5  |-  ( ( ( S `  C
)  e.  W  /\  Q  e.  ( 0 ... ( # `  ( S `  C )
) )  /\  V  e.  ( I  X.  2o ) )  ->  ( Q ( T `  ( S `  C ) ) V )  =  ( ( S `  C ) splice  <. Q ,  Q ,  <" V
( M `  V
) "> >. )
)
9613, 93, 94, 95syl3anc 1182 . . . 4  |-  ( ph  ->  ( Q ( T `
 ( S `  C ) ) V )  =  ( ( S `  C ) splice  <. Q ,  Q ,  <" V ( M `
 V ) "> >. ) )
97 swrdcl 11468 . . . . . 6  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o ) )
9834, 97syl 15 . . . . 5  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o ) )
99 wrd0 11434 . . . . . 6  |-  (/)  e. Word  (
I  X.  2o )
10099a1i 10 . . . . 5  |-  ( ph  -> 
(/)  e. Word  ( I  X.  2o ) )
1014efgmf 15038 . . . . . . . 8  |-  M :
( I  X.  2o )
--> ( I  X.  2o )
102101ffvelrni 5680 . . . . . . 7  |-  ( V  e.  ( I  X.  2o )  ->  ( M `
 V )  e.  ( I  X.  2o ) )
10394, 102syl 15 . . . . . 6  |-  ( ph  ->  ( M `  V
)  e.  ( I  X.  2o ) )
10494, 103s2cld 11535 . . . . 5  |-  ( ph  ->  <" V ( M `  V ) ">  e. Word  (
I  X.  2o ) )
105 eluzfz1 10819 . . . . . . . . . . . . . 14  |-  ( Q  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... Q
) )
10616, 105syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ( 0 ... Q ) )
10762zred 10133 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  Q  e.  RR )
108 nn0addge1 10026 . . . . . . . . . . . . . . . . 17  |-  ( ( Q  e.  RR  /\  2  e.  NN0 )  ->  Q  <_  ( Q  + 
2 ) )
109107, 41, 108sylancl 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  Q  <_  ( Q  +  2 ) )
110 eluz2 10252 . . . . . . . . . . . . . . . 16  |-  ( ( Q  +  2 )  e.  ( ZZ>= `  Q
)  <->  ( Q  e.  ZZ  /\  ( Q  +  2 )  e.  ZZ  /\  Q  <_ 
( Q  +  2 ) ) )
11162, 67, 109, 110syl3anbrc 1136 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Q  +  2 )  e.  ( ZZ>= `  Q ) )
112 uztrn 10260 . . . . . . . . . . . . . . 15  |-  ( ( P  e.  ( ZZ>= `  ( Q  +  2
) )  /\  ( Q  +  2 )  e.  ( ZZ>= `  Q
) )  ->  P  e.  ( ZZ>= `  Q )
)
11347, 111, 112syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  P  e.  ( ZZ>= `  Q ) )
114 elfzuzb 10808 . . . . . . . . . . . . . 14  |-  ( Q  e.  ( 0 ... P )  <->  ( Q  e.  ( ZZ>= `  0 )  /\  P  e.  ( ZZ>=
`  Q ) ) )
11516, 113, 114sylanbrc 645 . . . . . . . . . . . . 13  |-  ( ph  ->  Q  e.  ( 0 ... P ) )
116 ccatswrd 11475 . . . . . . . . . . . . 13  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  (
0  e.  ( 0 ... Q )  /\  Q  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `  ( A `  K )
) ) ) )  ->  ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) )  =  ( ( A `  K ) substr  <. 0 ,  P >. ) )
11734, 106, 115, 44, 116syl13anc 1184 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) )  =  ( ( A `  K ) substr  <. 0 ,  P >. ) )
118117oveq1d 5889 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) ) )
119 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o ) )
12034, 119syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o ) )
121 efgredlemb.u . . . . . . . . . . . . 13  |-  ( ph  ->  U  e.  ( I  X.  2o ) )
122101ffvelrni 5680 . . . . . . . . . . . . . 14  |-  ( U  e.  ( I  X.  2o )  ->  ( M `
 U )  e.  ( I  X.  2o ) )
123121, 122syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M `  U
)  e.  ( I  X.  2o ) )
124121, 123s2cld 11535 . . . . . . . . . . . 12  |-  ( ph  ->  <" U ( M `  U ) ">  e. Word  (
I  X.  2o ) )
125 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )  e. Word  ( I  X.  2o ) )
12634, 125syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  e. Word  ( I  X.  2o ) )
127 ccatass 11452 . . . . . . . . . . . 12  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ( M `  U ) ">  e. Word  (
I  X.  2o )  /\  ( ( A `
 K ) substr  <. P ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )  ->  ( (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> ) concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) ) )
128120, 124, 126, 127syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) ) )
129 efgredlemb.6 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  A
)  =  ( P ( T `  ( A `  K )
) U ) )
1302, 3, 4, 5efgtval 15048 . . . . . . . . . . . . . 14  |-  ( ( ( A `  K
)  e.  W  /\  P  e.  ( 0 ... ( # `  ( A `  K )
) )  /\  U  e.  ( I  X.  2o ) )  ->  ( P ( T `  ( A `  K ) ) U )  =  ( ( A `  K ) splice  <. P ,  P ,  <" U
( M `  U
) "> >. )
)
13133, 44, 121, 130syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P ( T `
 ( A `  K ) ) U )  =  ( ( A `  K ) splice  <. P ,  P ,  <" U ( M `
 U ) "> >. ) )
132 splval 11482 . . . . . . . . . . . . . 14  |-  ( ( ( A `  K
)  e.  W  /\  ( P  e.  (
0 ... ( # `  ( A `  K )
) )  /\  P  e.  ( 0 ... ( # `
 ( A `  K ) ) )  /\  <" U ( M `  U ) ">  e. Word  (
I  X.  2o ) ) )  ->  (
( A `  K
) splice  <. P ,  P ,  <" U ( M `  U ) "> >. )  =  ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U ( M `  U ) "> ) concat  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )
13333, 44, 44, 124, 132syl13anc 1184 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  K ) splice  <. P ,  P ,  <" U
( M `  U
) "> >. )  =  ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U ( M `  U ) "> ) concat  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )
134129, 131, 1333eqtrd 2332 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  A
)  =  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> ) concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )
135 efgredlemb.7 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  B
)  =  ( Q ( T `  ( B `  L )
) V ) )
1362, 3, 4, 5efgtval 15048 . . . . . . . . . . . . . 14  |-  ( ( ( B `  L
)  e.  W  /\  Q  e.  ( 0 ... ( # `  ( B `  L )
) )  /\  V  e.  ( I  X.  2o ) )  ->  ( Q ( T `  ( B `  L ) ) V )  =  ( ( B `  L ) splice  <. Q ,  Q ,  <" V
( M `  V
) "> >. )
)
13729, 14, 94, 136syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q ( T `
 ( B `  L ) ) V )  =  ( ( B `  L ) splice  <. Q ,  Q ,  <" V ( M `
 V ) "> >. ) )
138 splval 11482 . . . . . . . . . . . . . 14  |-  ( ( ( B `  L
)  e.  W  /\  ( Q  e.  (
0 ... ( # `  ( B `  L )
) )  /\  Q  e.  ( 0 ... ( # `
 ( B `  L ) ) )  /\  <" V ( M `  V ) ">  e. Word  (
I  X.  2o ) ) )  ->  (
( B `  L
) splice  <. Q ,  Q ,  <" V ( M `  V ) "> >. )  =  ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V ( M `  V ) "> ) concat  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
13929, 14, 14, 104, 138syl13anc 1184 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B `  L ) splice  <. Q ,  Q ,  <" V
( M `  V
) "> >. )  =  ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V ( M `  V ) "> ) concat  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
140135, 137, 1393eqtrd 2332 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  B
)  =  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> ) concat  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
14124, 134, 1403eqtr3d 2336 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
142118, 128, 1413eqtr2d 2334 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
143 swrdcl 11468 . . . . . . . . . . . 12  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. Q ,  P >. )  e. Word  ( I  X.  2o ) )
14434, 143syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A `  K ) substr  <. Q ,  P >. )  e. Word  (
I  X.  2o ) )
145 ccatcl 11445 . . . . . . . . . . . 12  |-  ( (
<" U ( M `
 U ) ">  e. Word  ( I  X.  2o )  /\  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  e. Word  ( I  X.  2o ) )  -> 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  e. Word 
( I  X.  2o ) )
146124, 126, 145syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )
147 ccatass 11452 . . . . . . . . . . 11  |-  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  ( ( A `
 K ) substr  <. Q ,  P >. )  e. Word  ( I  X.  2o )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )  -> 
( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) ) )
14898, 144, 146, 147syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) ) )
149 swrdcl 11468 . . . . . . . . . . . 12  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )  e. Word  ( I  X.  2o ) )
15030, 149syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. )  e. Word  ( I  X.  2o ) )
151 ccatass 11452 . . . . . . . . . . 11  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ( M `  V ) ">  e. Word  (
I  X.  2o )  /\  ( ( B `
 L ) substr  <. Q ,  ( # `  ( B `  L )
) >. )  e. Word  (
I  X.  2o ) )  ->  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> ) concat  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V ( M `  V ) "> concat  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) ) )
15232, 104, 150, 151syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( <" V ( M `  V ) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) ) )
153142, 148, 1523eqtr3d 2336 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat 
( <" V ( M `  V ) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) ) )
154 ccatcl 11445 . . . . . . . . . . 11  |-  ( ( ( ( A `  K ) substr  <. Q ,  P >. )  e. Word  (
I  X.  2o )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )  -> 
( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  e. Word 
( I  X.  2o ) )
155144, 146, 154syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  e. Word 
( I  X.  2o ) )
156 ccatcl 11445 . . . . . . . . . . 11  |-  ( (
<" V ( M `
 V ) ">  e. Word  ( I  X.  2o )  /\  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
)  e. Word  ( I  X.  2o ) )  -> 
( <" V ( M `  V ) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  e. Word 
( I  X.  2o ) )
157104, 150, 156syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)  e. Word  ( I  X.  2o ) )
158 uztrn 10260 . . . . . . . . . . . . . 14  |-  ( ( ( # `  ( A `  K )
)  e.  ( ZZ>= `  P )  /\  P  e.  ( ZZ>= `  Q )
)  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  Q ) )
15946, 113, 158syl2anc 642 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= `  Q ) )
160 elfzuzb 10808 . . . . . . . . . . . . 13  |-  ( Q  e.  ( 0 ... ( # `  ( A `  K )
) )  <->  ( Q  e.  ( ZZ>= `  0 )  /\  ( # `  ( A `  K )
)  e.  ( ZZ>= `  Q ) ) )
16116, 159, 160sylanbrc 645 . . . . . . . . . . . 12  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( A `  K )
) ) )
162 swrd0len 11471 . . . . . . . . . . . 12  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  Q  e.  ( 0 ... ( # `
 ( A `  K ) ) ) )  ->  ( # `  (
( A `  K
) substr  <. 0 ,  Q >. ) )  =  Q )
16334, 161, 162syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. 0 ,  Q >. ) )  =  Q )
164163, 40eqtr4d 2331 . . . . . . . . . 10  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. 0 ,  Q >. ) )  =  (
# `  ( ( B `  L ) substr  <.
0 ,  Q >. ) ) )
165 ccatopth 11478 . . . . . . . . . 10  |-  ( ( ( ( ( A `
 K ) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o )  /\  (
( ( A `  K ) substr  <. Q ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )  e. Word 
( I  X.  2o ) )  /\  (
( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)  e. Word  ( I  X.  2o ) )  /\  ( # `  ( ( A `  K ) substr  <. 0 ,  Q >. ) )  =  ( # `  ( ( B `  L ) substr  <. 0 ,  Q >. ) ) )  ->  ( ( ( ( A `  K
) substr  <. 0 ,  Q >. ) concat  ( ( ( A `  K ) substr  <. Q ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) ) )  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) )  <->  ( (
( A `  K
) substr  <. 0 ,  Q >. )  =  ( ( B `  L ) substr  <. 0 ,  Q >. )  /\  ( ( ( A `  K ) substr  <. Q ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) ) ) )
16698, 155, 32, 157, 164, 165syl221anc 1193 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat 
( <" V ( M `  V ) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )  <-> 
( ( ( A `
 K ) substr  <. 0 ,  Q >. )  =  ( ( B `
 L ) substr  <. 0 ,  Q >. )  /\  ( ( ( A `  K ) substr  <. Q ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) ) ) )
167153, 166mpbid 201 . . . . . . . 8  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. )  =  ( ( B `
 L ) substr  <. 0 ,  Q >. )  /\  ( ( ( A `  K ) substr  <. Q ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) ) )
168167simpld 445 . . . . . . 7  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  Q >. )  =  ( ( B `  L
) substr  <. 0 ,  Q >. ) )
169168oveq1d 5889 . . . . . 6  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
170 ccatrid 11451 . . . . . . . 8  |-  ( ( ( A `  K
) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o )  -> 
( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat  (/) )  =  ( ( A `  K ) substr  <. 0 ,  Q >. ) )
17198, 170syl 15 . . . . . . 7  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat  (/) )  =  ( ( A `  K ) substr  <. 0 ,  Q >. ) )
172171oveq1d 5889 . . . . . 6  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat  (/) ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
173169, 172, 173eqtr4rd 2339 . . . . 5  |-  ( ph  ->  ( S `  C
)  =  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat  (/) ) concat  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  (
# `  ( A `  K ) ) >.
) ) )
174163eqcomd 2301 . . . . 5  |-  ( ph  ->  Q  =  ( # `  ( ( A `  K ) substr  <. 0 ,  Q >. ) ) )
175 hash0 11371 . . . . . . 7  |-  ( # `  (/) )  =  0
176175oveq2i 5885 . . . . . 6  |-  ( Q  +  ( # `  (/) ) )  =  ( Q  + 
0 )
17763addid1d 9028 . . . . . 6  |-  ( ph  ->  ( Q  +  0 )  =  Q )
178176, 177syl5req 2341 . . . . 5  |-  ( ph  ->  Q  =  ( Q  +  ( # `  (/) ) ) )
17998, 100, 36, 104, 173, 174, 178splval2 11488 . . . 4  |-  ( ph  ->  ( ( S `  C ) splice  <. Q ,  Q ,  <" V
( M `  V
) "> >. )  =  ( ( ( ( A `  K
) substr  <. 0 ,  Q >. ) concat  <" V ( M `  V ) "> ) concat  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  (
# `  ( A `  K ) ) >.
) ) )
180 elfzuzb 10808 . . . . . . . . . . . . . 14  |-  ( Q  e.  ( 0 ... ( Q  +  2 ) )  <->  ( Q  e.  ( ZZ>= `  0 )  /\  ( Q  +  2 )  e.  ( ZZ>= `  Q ) ) )
18116, 111, 180sylanbrc 645 . . . . . . . . . . . . 13  |-  ( ph  ->  Q  e.  ( 0 ... ( Q  + 
2 ) ) )
182 elfzuzb 10808 . . . . . . . . . . . . . 14  |-  ( ( Q  +  2 )  e.  ( 0 ... P )  <->  ( ( Q  +  2 )  e.  ( ZZ>= `  0
)  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) ) )
18343, 47, 182sylanbrc 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q  +  2 )  e.  ( 0 ... P ) )
184 ccatswrd 11475 . . . . . . . . . . . . 13  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  ( Q  e.  ( 0 ... ( Q  + 
2 ) )  /\  ( Q  +  2
)  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `  ( A `  K )
) ) ) )  ->  ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) concat  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) )  =  ( ( A `  K ) substr  <. Q ,  P >. ) )
18534, 181, 183, 44, 184syl13anc 1184 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. ) concat  ( ( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. ) )  =  ( ( A `  K
) substr  <. Q ,  P >. ) )
186185oveq1d 5889 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) concat  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )
187 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
)  e. Word  ( I  X.  2o ) )
18834, 187syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. )  e. Word  (
I  X.  2o ) )
189 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. )  e. Word  ( I  X.  2o ) )
19034, 189syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. )  e. Word  (
I  X.  2o ) )
191 ccatass 11452 . . . . . . . . . . . 12  |-  ( ( ( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. )  e. Word  (
I  X.  2o )  /\  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. )  e. Word  ( I  X.  2o )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )  -> 
( ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) concat  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. ) concat  ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) ) ) )
192188, 190, 146, 191syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) concat  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) ) concat  ( <" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. ) concat  ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) ) ) )
193167simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. Q ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) )
194186, 192, 1933eqtr3d 2336 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. ) concat  ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) )
195 ccatcl 11445 . . . . . . . . . . . 12  |-  ( ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. )  e. Word  (
I  X.  2o )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )  -> 
( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  e. Word 
( I  X.  2o ) )
196190, 146, 195syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  e. Word 
( I  X.  2o ) )
197 swrdlen 11472 . . . . . . . . . . . . . 14  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  Q  e.  ( 0 ... ( Q  +  2 ) )  /\  ( Q  +  2 )  e.  ( 0 ... ( # `
 ( A `  K ) ) ) )  ->  ( # `  (
( A `  K
) substr  <. Q ,  ( Q  +  2 )
>. ) )  =  ( ( Q  +  2 )  -  Q ) )
19834, 181, 51, 197syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. Q ,  ( Q  +  2 )
>. ) )  =  ( ( Q  +  2 )  -  Q ) )
199 pncan2 9074 . . . . . . . . . . . . . 14  |-  ( ( Q  e.  CC  /\  2  e.  CC )  ->  ( ( Q  + 
2 )  -  Q
)  =  2 )
20063, 70, 199sylancl 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Q  + 
2 )  -  Q
)  =  2 )
201198, 200eqtrd 2328 . . . . . . . . . . . 12  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. Q ,  ( Q  +  2 )
>. ) )  =  2 )
202 s2len 11553 . . . . . . . . . . . 12  |-  ( # `  <" V ( M `  V ) "> )  =  2
203201, 202syl6eqr 2346 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. Q ,  ( Q  +  2 )
>. ) )  =  (
# `  <" V
( M `  V
) "> )
)
204 ccatopth 11478 . . . . . . . . . . 11  |-  ( ( ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. )  e. Word  ( I  X.  2o )  /\  ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  e. Word  ( I  X.  2o ) )  /\  ( <" V ( M `
 V ) ">  e. Word  ( I  X.  2o )  /\  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
)  e. Word  ( I  X.  2o ) )  /\  ( # `  ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) )  =  (
# `  <" V
( M `  V
) "> )
)  ->  ( (
( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. ) concat  ( (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. ) concat  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)  <->  ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
)  =  <" V
( M `  V
) ">  /\  (
( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )  =  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) ) ) )
205188, 196, 104, 150, 203, 204syl221anc 1193 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
) concat  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )  =  ( <" V
( M `  V
) "> concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)  <->  ( ( ( A `  K ) substr  <. Q ,  ( Q  +  2 ) >.
)  =  <" V
( M `  V
) ">  /\  (
( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )  =  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) ) ) )
206194, 205mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. Q ,  ( Q  + 
2 ) >. )  =  <" V ( M `  V ) ">  /\  (
( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )  =  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) ) )
207206simpld 445 . . . . . . . 8  |-  ( ph  ->  ( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. )  =  <" V ( M `  V ) "> )
208207oveq2d 5890 . . . . . . 7  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. ) )  =  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) )
209 ccatswrd 11475 . . . . . . . 8  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  (
0  e.  ( 0 ... Q )  /\  Q  e.  ( 0 ... ( Q  + 
2 ) )  /\  ( Q  +  2
)  e.  ( 0 ... ( # `  ( A `  K )
) ) ) )  ->  ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. ) )  =  ( ( A `  K ) substr  <. 0 ,  ( Q  +  2 ) >. ) )
21034, 106, 181, 51, 209syl13anc 1184 . . . . . . 7  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. Q , 
( Q  +  2 ) >. ) )  =  ( ( A `  K ) substr  <. 0 ,  ( Q  +  2 ) >. ) )
211208, 210eqtr3d 2330 . . . . . 6  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> )  =  ( ( A `  K
) substr  <. 0 ,  ( Q  +  2 )
>. ) )
212211oveq1d 5889 . . . . 5  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( ( A `  K
) substr  <. 0 ,  ( Q  +  2 )
>. ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
) )
213 eluzfz1 10819 . . . . . . 7  |-  ( ( Q  +  2 )  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... ( Q  +  2 ) ) )
21443, 213syl 15 . . . . . 6  |-  ( ph  ->  0  e.  ( 0 ... ( Q  + 
2 ) ) )
215 ccatswrd 11475 . . . . . 6  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  (
0  e.  ( 0 ... ( Q  + 
2 ) )  /\  ( Q  +  2
)  e.  ( 0 ... ( # `  ( A `  K )
) )  /\  ( # `
 ( A `  K ) )  e.  ( 0 ... ( # `
 ( A `  K ) ) ) ) )  ->  (
( ( A `  K ) substr  <. 0 ,  ( Q  +  2 ) >. ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K
) ) >. )
)
21634, 214, 51, 57, 215syl13anc 1184 . . . . 5  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  ( Q  +  2 ) >.
) concat  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K )
) >. ) )
217 swrdid 11474 . . . . . 6  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K
) ) >. )  =  ( A `  K ) )
21834, 217syl 15 . . . . 5  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K )
) >. )  =  ( A `  K ) )
219212, 216, 2183eqtrd 2332 . . . 4  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
)  =  ( A `
 K ) )
22096, 179, 2193eqtrd 2332 . . 3  |-  ( ph  ->  ( Q ( T `
 ( S `  C ) ) V )  =  ( A `
 K ) )
2212, 3, 4, 5efgtf 15047 . . . . . . 7  |-  ( ( S `  C )  e.  W  ->  (
( T `  ( S `  C )
)  =  ( a  e.  ( 0 ... ( # `  ( S `  C )
) ) ,  i  e.  ( I  X.  2o )  |->  ( ( S `  C ) splice  <. a ,  a , 
<" i ( M `
 i ) "> >. ) )  /\  ( T `  ( S `
 C ) ) : ( ( 0 ... ( # `  ( S `  C )
) )  X.  (
I  X.  2o ) ) --> W ) )
22213, 221syl 15 . . . . . 6  |-  ( ph  ->  ( ( T `  ( S `  C ) )  =  ( a  e.  ( 0 ... ( # `  ( S `  C )
) ) ,  i  e.  ( I  X.  2o )  |->  ( ( S `  C ) splice  <. a ,  a , 
<" i ( M `
 i ) "> >. ) )  /\  ( T `  ( S `
 C ) ) : ( ( 0 ... ( # `  ( S `  C )
) )  X.  (
I  X.  2o ) ) --> W ) )
223222simprd 449 . . . . 5  |-  ( ph  ->  ( T `  ( S `  C )
) : ( ( 0 ... ( # `  ( S `  C
) ) )  X.  ( I  X.  2o ) ) --> W )
224 ffn 5405 . . . . 5  |-  ( ( T `  ( S `
 C ) ) : ( ( 0 ... ( # `  ( S `  C )
) )  X.  (
I  X.  2o ) ) --> W  ->  ( T `  ( S `  C ) )  Fn  ( ( 0 ... ( # `  ( S `  C )
) )  X.  (
I  X.  2o ) ) )
225223, 224syl 15 . . . 4  |-  ( ph  ->  ( T `  ( S `  C )
)  Fn  ( ( 0 ... ( # `  ( S `  C
) ) )  X.  ( I  X.  2o ) ) )
226 fnovrn 6011 . . . 4  |-  ( ( ( T `  ( S `  C )
)  Fn  ( ( 0 ... ( # `  ( S `  C
) ) )  X.  ( I  X.  2o ) )  /\  Q  e.  ( 0 ... ( # `
 ( S `  C ) ) )  /\  V  e.  ( I  X.  2o ) )  ->  ( Q
( T `  ( S `  C )
) V )  e. 
ran  ( T `  ( S `  C ) ) )
227225, 93, 94, 226syl3anc 1182 . . 3  |-  ( ph  ->  ( Q ( T `
 ( S `  C ) ) V )  e.  ran  ( T `  ( S `  C ) ) )
228220, 227eqeltrrd 2371 . 2  |-  ( ph  ->  ( A `  K
)  e.  ran  ( T `  ( S `  C ) ) )
229 uztrn 10260 . . . . . . 7  |-  ( ( ( P  -  2 )  e.  ( ZZ>= `  Q )  /\  Q  e.  ( ZZ>= `  0 )
)  ->  ( P  -  2 )  e.  ( ZZ>= `  0 )
)
23089, 16, 229syl2anc 642 . . . . . 6  |-  ( ph  ->  ( P  -  2 )  e.  ( ZZ>= ` 
0 ) )
231 elfzuzb 10808 . . . . . 6  |-  ( ( P  -  2 )  e.  ( 0 ... ( # `  ( S `  C )
) )  <->  ( ( P  -  2 )  e.  ( ZZ>= `  0
)  /\  ( # `  ( S `  C )
)  e.  ( ZZ>= `  ( P  -  2
) ) ) )
232230, 87, 231sylanbrc 645 . . . . 5  |-  ( ph  ->  ( P  -  2 )  e.  ( 0 ... ( # `  ( S `  C )
) ) )
2332, 3, 4, 5efgtval 15048 . . . . 5  |-  ( ( ( S `  C
)  e.  W  /\  ( P  -  2
)  e.  ( 0 ... ( # `  ( S `  C )
) )  /\  U  e.  ( I  X.  2o ) )  ->  (
( P  -  2 ) ( T `  ( S `  C ) ) U )  =  ( ( S `  C ) splice  <. ( P  -  2 ) ,  ( P  -  2 ) ,  <" U
( M `  U
) "> >. )
)
23413, 232, 121, 233syl3anc 1182 . . . 4  |-  ( ph  ->  ( ( P  - 
2 ) ( T `
 ( S `  C ) ) U )  =  ( ( S `  C ) splice  <. ( P  -  2 ) ,  ( P  -  2 ) , 
<" U ( M `
 U ) "> >. ) )
235 swrdcl 11468 . . . . . 6  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. 0 ,  ( P  -  2 ) >.
)  e. Word  ( I  X.  2o ) )
23630, 235syl 15 . . . . 5  |-  ( ph  ->  ( ( B `  L ) substr  <. 0 ,  ( P  -  2 ) >. )  e. Word  (
I  X.  2o ) )
237 swrdcl 11468 . . . . . 6  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. P ,  ( # `  ( B `  L
) ) >. )  e. Word  ( I  X.  2o ) )
23830, 237syl 15 . . . . 5  |-  ( ph  ->  ( ( B `  L ) substr  <. P , 
( # `  ( B `
 L ) )
>. )  e. Word  ( I  X.  2o ) )
239 ccatswrd 11475 . . . . . . . . . . 11  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  (
( Q  +  2 )  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `  ( A `  K )
) )  /\  ( # `
 ( A `  K ) )  e.  ( 0 ... ( # `
 ( A `  K ) ) ) ) )  ->  (
( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )
24034, 183, 44, 57, 239syl13anc 1184 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( A `  K
) substr  <. ( Q  + 
2 ) ,  (
# `  ( A `  K ) ) >.
) )
241206simprd 449 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) )
242 elfzuzb 10808 . . . . . . . . . . . . . . . 16  |-  ( Q  e.  ( 0 ... ( P  -  2 ) )  <->  ( Q  e.  ( ZZ>= `  0 )  /\  ( P  -  2 )  e.  ( ZZ>= `  Q ) ) )
24316, 89, 242sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Q  e.  ( 0 ... ( P  - 
2 ) ) )
2442, 3, 4, 5, 6, 7, 21, 22, 23, 24, 25, 26, 27, 44, 14, 121, 94, 129, 135efgredlemg 15067 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( # `  ( A `  K )
)  =  ( # `  ( B `  L
) ) )
245244, 46eqeltrrd 2371 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( ZZ>= `  P ) )
24641nn0ge0i 10009 . . . . . . . . . . . . . . . . . . . 20  |-  0  <_  2
247246a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  2 )
24876zred 10133 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  P  e.  RR )
249 2re 9831 . . . . . . . . . . . . . . . . . . . 20  |-  2  e.  RR
250 subge02 9305 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( P  e.  RR  /\  2  e.  RR )  ->  ( 0  <_  2  <->  ( P  -  2 )  <_  P ) )
251248, 249, 250sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 0  <_  2  <->  ( P  -  2 )  <_  P ) )
252247, 251mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( P  -  2 )  <_  P )
253 eluz2 10252 . . . . . . . . . . . . . . . . . 18  |-  ( P  e.  ( ZZ>= `  ( P  -  2 ) )  <->  ( ( P  -  2 )  e.  ZZ  /\  P  e.  ZZ  /\  ( P  -  2 )  <_  P ) )
25478, 76, 252, 253syl3anbrc 1136 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  P  e.  ( ZZ>= `  ( P  -  2
) ) )
255 uztrn 10260 . . . . . . . . . . . . . . . . 17  |-  ( ( ( # `  ( B `  L )
)  e.  ( ZZ>= `  P )  /\  P  e.  ( ZZ>= `  ( P  -  2 ) ) )  ->  ( # `  ( B `  L )
)  e.  ( ZZ>= `  ( P  -  2
) ) )
256245, 254, 255syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( ZZ>= `  ( P  -  2
) ) )
257 elfzuzb 10808 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  2 )  e.  ( 0 ... ( # `  ( B `  L )
) )  <->  ( ( P  -  2 )  e.  ( ZZ>= `  0
)  /\  ( # `  ( B `  L )
)  e.  ( ZZ>= `  ( P  -  2
) ) ) )
258230, 256, 257sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( P  -  2 )  e.  ( 0 ... ( # `  ( B `  L )
) ) )
259 lencl 11437 . . . . . . . . . . . . . . . . . 18  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( # `  ( B `  L
) )  e.  NN0 )
26030, 259syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  NN0 )
261260, 54syl6eleq 2386 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( ZZ>= ` 
0 ) )
262 eluzfz2 10820 . . . . . . . . . . . . . . . 16  |-  ( (
# `  ( B `  L ) )  e.  ( ZZ>= `  0 )  ->  ( # `  ( B `  L )
)  e.  ( 0 ... ( # `  ( B `  L )
) ) )
263261, 262syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( 0 ... ( # `  ( B `  L )
) ) )
264 ccatswrd 11475 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  ( Q  e.  ( 0 ... ( P  - 
2 ) )  /\  ( P  -  2
)  e.  ( 0 ... ( # `  ( B `  L )
) )  /\  ( # `
 ( B `  L ) )  e.  ( 0 ... ( # `
 ( B `  L ) ) ) ) )  ->  (
( ( B `  L ) substr  <. Q , 
( P  -  2 ) >. ) concat  ( ( B `  L ) substr  <.
( P  -  2 ) ,  ( # `  ( B `  L
) ) >. )
)  =  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)
26530, 243, 258, 263, 264syl13anc 1184 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. Q ,  ( P  - 
2 ) >. ) concat  ( ( B `  L
) substr  <. ( P  - 
2 ) ,  (
# `  ( B `  L ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) )
266241, 265eqtr4d 2331 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  (
<" U ( M `
 U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( B `
 L ) substr  <. Q ,  ( P  - 
2 ) >. ) concat  ( ( B `  L
) substr  <. ( P  - 
2 ) ,  (
# `  ( B `  L ) ) >.
) ) )
267 swrdcl 11468 . . . . . . . . . . . . . . 15  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
)  e. Word  ( I  X.  2o ) )
26830, 267syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B `  L ) substr  <. Q , 
( P  -  2 ) >. )  e. Word  (
I  X.  2o ) )
269 swrdcl 11468 . . . . . . . . . . . . . . 15  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L
) ) >. )  e. Word  ( I  X.  2o ) )
27030, 269syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L )
) >. )  e. Word  (
I  X.  2o ) )
271 swrdlen 11472 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  ( Q  +  2 )  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `
 ( A `  K ) ) ) )  ->  ( # `  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. ) )  =  ( P  -  ( Q  +  2 ) ) )
27234, 183, 44, 271syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. ) )  =  ( P  -  ( Q  +  2 ) ) )
273 swrdlen 11472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  Q  e.  ( 0 ... ( P  -  2 ) )  /\  ( P  -  2 )  e.  ( 0 ... ( # `
 ( B `  L ) ) ) )  ->  ( # `  (
( B `  L
) substr  <. Q ,  ( P  -  2 )
>. ) )  =  ( ( P  -  2 )  -  Q ) )
27430, 243, 258, 273syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  (
( B `  L
) substr  <. Q ,  ( P  -  2 )
>. ) )  =  ( ( P  -  2 )  -  Q ) )
27580, 63, 71sub32d 9205 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( P  -  Q )  -  2 )  =  ( ( P  -  2 )  -  Q ) )
27680, 63, 71subsub4d 9204 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( P  -  Q )  -  2 )  =  ( P  -  ( Q  + 
2 ) ) )
277274, 275, 2763eqtr2d 2334 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
( B `  L
) substr  <. Q ,  ( P  -  2 )
>. ) )  =  ( P  -  ( Q  +  2 ) ) )
278272, 277eqtr4d 2331 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. ) )  =  (
# `  ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
) ) )
279 ccatopth 11478 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. )  e. Word  ( I  X.  2o )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )  /\  ( ( ( B `
 L ) substr  <. Q ,  ( P  - 
2 ) >. )  e. Word  ( I  X.  2o )  /\  ( ( B `
 L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L )
) >. )  e. Word  (
I  X.  2o ) )  /\  ( # `  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) )  =  ( # `  (
( B `  L
) substr  <. Q ,  ( P  -  2 )
>. ) ) )  -> 
( ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  =  ( ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
) concat  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L )
) >. ) )  <->  ( (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. )  =  ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
)  /\  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. ( P  - 
2 ) ,  (
# `  ( B `  L ) ) >.
) ) ) )
280190, 146, 268, 270, 278, 279syl221anc 1193 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. ) concat 
( <" U ( M `  U ) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) ) )  =  ( ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
) concat  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L )
) >. ) )  <->  ( (
( A `  K
) substr  <. ( Q  + 
2 ) ,  P >. )  =  ( ( B `  L ) substr  <. Q ,  ( P  -  2 ) >.
)  /\  ( <" U ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. ( P  - 
2 ) ,  (
# `  ( B `  L ) ) >.
) ) ) )
281266, 280mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. )  =  ( ( B `
 L ) substr  <. Q ,  ( P  - 
2 ) >. )  /\  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L
) ) >. )
) )
282281simpld 445 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  P >. )  =  ( ( B `  L
) substr  <. Q ,  ( P  -  2 )
>. ) )
283281simprd 449 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L
) ) >. )
)
284 elfzuzb 10808 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  2 )  e.  ( 0 ... P )  <->  ( ( P  -  2 )  e.  ( ZZ>= `  0
)  /\  P  e.  ( ZZ>= `  ( P  -  2 ) ) ) )
285230, 254, 284sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( P  -  2 )  e.  ( 0 ... P ) )
286 elfzuz 10810 . . . . . . . . . . . . . . . . 17  |-  ( P  e.  ( 0 ... ( # `  ( A `  K )
) )  ->  P  e.  ( ZZ>= `  0 )
)
28744, 286syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  P  e.  ( ZZ>= ` 
0 ) )
288 elfzuzb 10808 . . . . . . . . . . . . . . . 16  |-  ( P  e.  ( 0 ... ( # `  ( B `  L )
) )  <->  ( P  e.  ( ZZ>= `  0 )  /\  ( # `  ( B `  L )
)  e.  ( ZZ>= `  P ) ) )
289287, 245, 288sylanbrc 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  ( 0 ... ( # `  ( B `  L )
) ) )
290 ccatswrd 11475 . . . . . . . . . . . . . . 15  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  (
( P  -  2 )  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `  ( B `  L )
) )  /\  ( # `
 ( B `  L ) )  e.  ( 0 ... ( # `
 ( B `  L ) ) ) ) )  ->  (
( ( B `  L ) substr  <. ( P  -  2 ) ,  P >. ) concat  ( ( B `  L ) substr  <. P ,  ( # `  ( B `  L )
) >. ) )  =  ( ( B `  L ) substr  <. ( P  -  2 ) ,  ( # `  ( B `  L )
) >. ) )
29130, 285, 289, 263, 290syl13anc 1184 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. ( P  -  2 ) ,  P >. ) concat  ( ( B `  L
) substr  <. P ,  (
# `  ( B `  L ) ) >.
) )  =  ( ( B `  L
) substr  <. ( P  - 
2 ) ,  (
# `  ( B `  L ) ) >.
) )
292283, 291eqtr4d 2331 . . . . . . . . . . . . 13  |-  ( ph  ->  ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( ( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) concat  ( ( B `
 L ) substr  <. P ,  ( # `  ( B `  L )
) >. ) ) )
293 swrdcl 11468 . . . . . . . . . . . . . . 15  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. ( P  -  2 ) ,  P >. )  e. Word  ( I  X.  2o ) )
29430, 293syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( B `  L ) substr  <. ( P  -  2 ) ,  P >. )  e. Word  (
I  X.  2o ) )
295 s2len 11553 . . . . . . . . . . . . . . 15  |-  ( # `  <" U ( M `  U ) "> )  =  2
296 swrdlen 11472 . . . . . . . . . . . . . . . . 17  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  ( P  -  2 )  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `
 ( B `  L ) ) ) )  ->  ( # `  (
( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) )  =  ( P  -  ( P  -  2 ) ) )
29730, 285, 289, 296syl3anc 1182 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( # `  (
( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) )  =  ( P  -  ( P  -  2 ) ) )
298 nncan 9092 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  CC  /\  2  e.  CC )  ->  ( P  -  ( P  -  2 ) )  =  2 )
29980, 70, 298sylancl 643 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P  -  ( P  -  2 ) )  =  2 )
300297, 299eqtr2d 2329 . . . . . . . . . . . . . . 15  |-  ( ph  ->  2  =  ( # `  ( ( B `  L ) substr  <. ( P  -  2 ) ,  P >. ) ) )
301295, 300syl5eq 2340 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  <" U ( M `  U ) "> )  =  ( # `  (
( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) ) )
302 ccatopth 11478 . . . . . . . . . . . . . 14  |-  ( ( ( <" U
( M `  U
) ">  e. Word  ( I  X.  2o )  /\  ( ( A `
 K ) substr  <. P ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )  /\  ( ( ( B `  L
) substr  <. ( P  - 
2 ) ,  P >. )  e. Word  ( I  X.  2o )  /\  ( ( B `  L ) substr  <. P , 
( # `  ( B `
 L ) )
>. )  e. Word  ( I  X.  2o ) )  /\  ( # `  <" U ( M `  U ) "> )  =  ( # `  (
( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) ) )  -> 
( ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( ( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) concat  ( ( B `
 L ) substr  <. P ,  ( # `  ( B `  L )
) >. ) )  <->  ( <" U ( M `  U ) ">  =  ( ( B `
 L ) substr  <. ( P  -  2 ) ,  P >. )  /\  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  =  (
( B `  L
) substr  <. P ,  (
# `  ( B `  L ) ) >.
) ) ) )
303124, 126, 294, 238, 301, 302syl221anc 1193 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( <" U
( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  =  ( ( ( B `  L
) substr  <. ( P  - 
2 ) ,  P >. ) concat  ( ( B `
 L ) substr  <. P ,  ( # `  ( B `  L )
) >. ) )  <->  ( <" U ( M `  U ) ">  =  ( ( B `
 L ) substr  <. ( P  -  2 ) ,  P >. )  /\  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  =  (
( B `  L
) substr  <. P ,  (
# `  ( B `  L ) ) >.
) ) ) )
304292, 303mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( <" U
( M `  U
) ">  =  ( ( B `  L ) substr  <. ( P  -  2 ) ,  P >. )  /\  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  =  ( ( B `  L ) substr  <. P ,  ( # `  ( B `  L
) ) >. )
) )
305304simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  =  (
( B `  L
) substr  <. P ,  (
# `  ( B `  L ) ) >.
) )
306282, 305oveq12d 5892 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  P >. ) concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( ( B `  L ) substr  <. Q , 
( P  -  2 ) >. ) concat  ( ( B `  L ) substr  <. P ,  ( # `  ( B `  L )
) >. ) ) )
307240, 306eqtr3d 2330 . . . . . . . . 9  |-  ( ph  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. )  =  ( (