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

Theorem efgredlemc 15070
Description: The reduced word that forms the base of the sequence in efgsval 15056 is uniquely determined, given the ending representation. (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 ) )
Assertion
Ref Expression
efgredlemc  |-  ( ph  ->  ( P  e.  (
ZZ>= `  Q )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
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    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 efgredlemc
Dummy variables  c 
i are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzp1 10277 . 2  |-  ( P  e.  ( ZZ>= `  Q
)  ->  ( P  =  Q  \/  P  e.  ( ZZ>= `  ( Q  +  1 ) ) ) )
2 efgredlemb.8 . . . . . 6  |-  ( ph  ->  -.  ( A `  K )  =  ( B `  L ) )
3 efgval.w . . . . . . . . . . 11  |-  W  =  (  _I  ` Word  ( I  X.  2o ) )
4 fviss 5596 . . . . . . . . . . 11  |-  (  _I 
` Word  ( I  X.  2o ) )  C_ Word  ( I  X.  2o )
53, 4eqsstri 3221 . . . . . . . . . 10  |-  W  C_ Word  ( I  X.  2o )
6 efgredlem.2 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  dom  S
)
7 efgval.r . . . . . . . . . . . . . . 15  |-  .~  =  ( ~FG  `  I )
8 efgval2.m . . . . . . . . . . . . . . 15  |-  M  =  ( y  e.  I ,  z  e.  2o  |->  <. y ,  ( 1o 
\  z ) >.
)
9 efgval2.t . . . . . . . . . . . . . . 15  |-  T  =  ( v  e.  W  |->  ( n  e.  ( 0 ... ( # `  v ) ) ,  w  e.  ( I  X.  2o )  |->  ( v splice  <. n ,  n ,  <" w ( M `  w ) "> >. )
) )
10 efgred.d . . . . . . . . . . . . . . 15  |-  D  =  ( W  \  U_ x  e.  W  ran  ( T `  x ) )
11 efgred.s . . . . . . . . . . . . . . 15  |-  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 ) ) )
123, 7, 8, 9, 10, 11efgsdm 15055 . . . . . . . . . . . . . 14  |-  ( A  e.  dom  S  <->  ( A  e.  (Word  W  \  { (/)
} )  /\  ( A `  0 )  e.  D  /\  A. i  e.  ( 1..^ ( # `  A ) ) ( A `  i )  e.  ran  ( T `
 ( A `  ( i  -  1 ) ) ) ) )
1312simp1bi 970 . . . . . . . . . . . . 13  |-  ( A  e.  dom  S  ->  A  e.  (Word  W  \  { (/) } ) )
146, 13syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  (Word  W  \  { (/) } ) )
15 eldifi 3311 . . . . . . . . . . . 12  |-  ( A  e.  (Word  W  \  { (/) } )  ->  A  e. Word  W )
16 wrdf 11435 . . . . . . . . . . . 12  |-  ( A  e. Word  W  ->  A : ( 0..^ (
# `  A )
) --> W )
1714, 15, 163syl 18 . . . . . . . . . . 11  |-  ( ph  ->  A : ( 0..^ ( # `  A
) ) --> W )
18 fzossfz 10908 . . . . . . . . . . . . 13  |-  ( 0..^ ( ( # `  A
)  -  1 ) )  C_  ( 0 ... ( ( # `  A )  -  1 ) )
19 efgredlemb.k . . . . . . . . . . . . . 14  |-  K  =  ( ( ( # `  A )  -  1 )  -  1 )
20 efgredlem.1 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  A. a  e.  dom  S A. b  e.  dom  S ( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  ->  ( ( S `  a )  =  ( S `  b )  ->  (
a `  0 )  =  ( b ` 
0 ) ) ) )
21 efgredlem.3 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  S
)
22 efgredlem.4 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( S `  A
)  =  ( S `
 B ) )
23 efgredlem.5 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  -.  ( A ` 
0 )  =  ( B `  0 ) )
243, 7, 8, 9, 10, 11, 20, 6, 21, 22, 23efgredlema 15065 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( # `  A )  -  1 )  e.  NN  /\  ( ( # `  B
)  -  1 )  e.  NN ) )
2524simpld 445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( # `  A
)  -  1 )  e.  NN )
26 fzo0end 10931 . . . . . . . . . . . . . . 15  |-  ( ( ( # `  A
)  -  1 )  e.  NN  ->  (
( ( # `  A
)  -  1 )  -  1 )  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )
2725, 26syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( # `  A )  -  1 )  -  1 )  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )
2819, 27syl5eqel 2380 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )
2918, 28sseldi 3191 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  ( 0 ... ( ( # `  A )  -  1 ) ) )
30 lencl 11437 . . . . . . . . . . . . . . 15  |-  ( A  e. Word  W  ->  ( # `
 A )  e. 
NN0 )
3114, 15, 303syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  A
)  e.  NN0 )
3231nn0zd 10131 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  A
)  e.  ZZ )
33 fzoval 10892 . . . . . . . . . . . . 13  |-  ( (
# `  A )  e.  ZZ  ->  ( 0..^ ( # `  A
) )  =  ( 0 ... ( (
# `  A )  -  1 ) ) )
3432, 33syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0..^ ( # `  A ) )  =  ( 0 ... (
( # `  A )  -  1 ) ) )
3529, 34eleqtrrd 2373 . . . . . . . . . . 11  |-  ( ph  ->  K  e.  ( 0..^ ( # `  A
) ) )
36 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( A : ( 0..^ ( # `  A
) ) --> W  /\  K  e.  ( 0..^ ( # `  A
) ) )  -> 
( A `  K
)  e.  W )
3717, 35, 36syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( A `  K
)  e.  W )
385, 37sseldi 3191 . . . . . . . . 9  |-  ( ph  ->  ( A `  K
)  e. Word  ( I  X.  2o ) )
39 efgredlemb.p . . . . . . . . . 10  |-  ( ph  ->  P  e.  ( 0 ... ( # `  ( A `  K )
) ) )
40 elfzuz 10810 . . . . . . . . . 10  |-  ( P  e.  ( 0 ... ( # `  ( A `  K )
) )  ->  P  e.  ( ZZ>= `  0 )
)
41 eluzfz1 10819 . . . . . . . . . 10  |-  ( P  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... P
) )
4239, 40, 413syl 18 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0 ... P ) )
43 lencl 11437 . . . . . . . . . . . 12  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( # `  ( A `  K
) )  e.  NN0 )
4438, 43syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  NN0 )
45 nn0uz 10278 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
4644, 45syl6eleq 2386 . . . . . . . . . 10  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( ZZ>= ` 
0 ) )
47 eluzfz2 10820 . . . . . . . . . 10  |-  ( (
# `  ( A `  K ) )  e.  ( ZZ>= `  0 )  ->  ( # `  ( A `  K )
)  e.  ( 0 ... ( # `  ( A `  K )
) ) )
4846, 47syl 15 . . . . . . . . 9  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  ( 0 ... ( # `  ( A `  K )
) ) )
49 ccatswrd 11475 . . . . . . . . 9  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  (
0  e.  ( 0 ... P )  /\  P  e.  ( 0 ... ( # `  ( A `  K )
) )  /\  ( # `
 ( A `  K ) )  e.  ( 0 ... ( # `
 ( A `  K ) ) ) ) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K )
) >. ) )
5038, 42, 39, 48, 49syl13anc 1184 . . . . . . . 8  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat 
( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( ( A `  K
) substr  <. 0 ,  (
# `  ( A `  K ) ) >.
) )
51 swrdid 11474 . . . . . . . . 9  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K
) ) >. )  =  ( A `  K ) )
5238, 51syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  ( # `  ( A `  K )
) >. )  =  ( A `  K ) )
5350, 52eqtrd 2328 . . . . . . 7  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat 
( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( A `  K ) )
543, 7, 8, 9, 10, 11efgsdm 15055 . . . . . . . . . . . . . 14  |-  ( B  e.  dom  S  <->  ( B  e.  (Word  W  \  { (/)
} )  /\  ( B `  0 )  e.  D  /\  A. i  e.  ( 1..^ ( # `  B ) ) ( B `  i )  e.  ran  ( T `
 ( B `  ( i  -  1 ) ) ) ) )
5554simp1bi 970 . . . . . . . . . . . . 13  |-  ( B  e.  dom  S  ->  B  e.  (Word  W  \  { (/) } ) )
5621, 55syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  (Word  W  \  { (/) } ) )
57 eldifi 3311 . . . . . . . . . . . 12  |-  ( B  e.  (Word  W  \  { (/) } )  ->  B  e. Word  W )
58 wrdf 11435 . . . . . . . . . . . 12  |-  ( B  e. Word  W  ->  B : ( 0..^ (
# `  B )
) --> W )
5956, 57, 583syl 18 . . . . . . . . . . 11  |-  ( ph  ->  B : ( 0..^ ( # `  B
) ) --> W )
60 fzossfz 10908 . . . . . . . . . . . . 13  |-  ( 0..^ ( ( # `  B
)  -  1 ) )  C_  ( 0 ... ( ( # `  B )  -  1 ) )
61 efgredlemb.l . . . . . . . . . . . . . 14  |-  L  =  ( ( ( # `  B )  -  1 )  -  1 )
6224simprd 449 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( # `  B
)  -  1 )  e.  NN )
63 fzo0end 10931 . . . . . . . . . . . . . . 15  |-  ( ( ( # `  B
)  -  1 )  e.  NN  ->  (
( ( # `  B
)  -  1 )  -  1 )  e.  ( 0..^ ( (
# `  B )  -  1 ) ) )
6462, 63syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( # `  B )  -  1 )  -  1 )  e.  ( 0..^ ( ( # `  B
)  -  1 ) ) )
6561, 64syl5eqel 2380 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  ( 0..^ ( ( # `  B
)  -  1 ) ) )
6660, 65sseldi 3191 . . . . . . . . . . . 12  |-  ( ph  ->  L  e.  ( 0 ... ( ( # `  B )  -  1 ) ) )
67 lencl 11437 . . . . . . . . . . . . . . 15  |-  ( B  e. Word  W  ->  ( # `
 B )  e. 
NN0 )
6856, 57, 673syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( # `  B
)  e.  NN0 )
6968nn0zd 10131 . . . . . . . . . . . . 13  |-  ( ph  ->  ( # `  B
)  e.  ZZ )
70 fzoval 10892 . . . . . . . . . . . . 13  |-  ( (
# `  B )  e.  ZZ  ->  ( 0..^ ( # `  B
) )  =  ( 0 ... ( (
# `  B )  -  1 ) ) )
7169, 70syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0..^ ( # `  B ) )  =  ( 0 ... (
( # `  B )  -  1 ) ) )
7266, 71eleqtrrd 2373 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  ( 0..^ ( # `  B
) ) )
73 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( B : ( 0..^ ( # `  B
) ) --> W  /\  L  e.  ( 0..^ ( # `  B
) ) )  -> 
( B `  L
)  e.  W )
7459, 72, 73syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( B `  L
)  e.  W )
755, 74sseldi 3191 . . . . . . . . 9  |-  ( ph  ->  ( B `  L
)  e. Word  ( I  X.  2o ) )
76 efgredlemb.q . . . . . . . . . 10  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( B `  L )
) ) )
77 elfzuz 10810 . . . . . . . . . 10  |-  ( Q  e.  ( 0 ... ( # `  ( B `  L )
) )  ->  Q  e.  ( ZZ>= `  0 )
)
78 eluzfz1 10819 . . . . . . . . . 10  |-  ( Q  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... Q
) )
7976, 77, 783syl 18 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0 ... Q ) )
80 lencl 11437 . . . . . . . . . . . 12  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( # `  ( B `  L
) )  e.  NN0 )
8175, 80syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  NN0 )
8281, 45syl6eleq 2386 . . . . . . . . . 10  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( ZZ>= ` 
0 ) )
83 eluzfz2 10820 . . . . . . . . . 10  |-  ( (
# `  ( B `  L ) )  e.  ( ZZ>= `  0 )  ->  ( # `  ( B `  L )
)  e.  ( 0 ... ( # `  ( B `  L )
) ) )
8482, 83syl 15 . . . . . . . . 9  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  ( 0 ... ( # `  ( B `  L )
) ) )
85 ccatswrd 11475 . . . . . . . . 9  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  (
0  e.  ( 0 ... Q )  /\  Q  e.  ( 0 ... ( # `  ( B `  L )
) )  /\  ( # `
 ( B `  L ) )  e.  ( 0 ... ( # `
 ( B `  L ) ) ) ) )  ->  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  =  ( ( B `  L ) substr  <. 0 ,  ( # `  ( B `  L )
) >. ) )
8675, 79, 76, 84, 85syl13anc 1184 . . . . . . . 8  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) )  =  ( ( B `  L
) substr  <. 0 ,  (
# `  ( B `  L ) ) >.
) )
87 swrdid 11474 . . . . . . . . 9  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. 0 ,  ( # `  ( B `  L
) ) >. )  =  ( B `  L ) )
8875, 87syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( B `  L ) substr  <. 0 ,  ( # `  ( B `  L )
) >. )  =  ( B `  L ) )
8986, 88eqtrd 2328 . . . . . . 7  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) )  =  ( B `  L ) )
9053, 89eqeq12d 2310 . . . . . 6  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat 
( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  <->  ( A `  K )  =  ( B `  L ) ) )
912, 90mtbird 292 . . . . 5  |-  ( ph  ->  -.  ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat 
( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
92 efgredlemb.6 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  A
)  =  ( P ( T `  ( A `  K )
) U ) )
93 efgredlemb.u . . . . . . . . . . . . . 14  |-  ( ph  ->  U  e.  ( I  X.  2o ) )
943, 7, 8, 9efgtval 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
) "> >. )
)
9537, 39, 93, 94syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P ( T `
 ( A `  K ) ) U )  =  ( ( A `  K ) splice  <. P ,  P ,  <" U ( M `
 U ) "> >. ) )
968efgmf 15038 . . . . . . . . . . . . . . . . 17  |-  M :
( I  X.  2o )
--> ( I  X.  2o )
9796ffvelrni 5680 . . . . . . . . . . . . . . . 16  |-  ( U  e.  ( I  X.  2o )  ->  ( M `
 U )  e.  ( I  X.  2o ) )
9893, 97syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( M `  U
)  e.  ( I  X.  2o ) )
9993, 98s2cld 11535 . . . . . . . . . . . . . 14  |-  ( ph  ->  <" U ( M `  U ) ">  e. Word  (
I  X.  2o ) )
100 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 ) ) >.
) ) )
10137, 39, 39, 99, 100syl13anc 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 ) ) >.
) ) )
10292, 95, 1013eqtrd 2332 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  A
)  =  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> ) concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )
103 efgredlemb.7 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S `  B
)  =  ( Q ( T `  ( B `  L )
) V ) )
104 efgredlemb.v . . . . . . . . . . . . . 14  |-  ( ph  ->  V  e.  ( I  X.  2o ) )
1053, 7, 8, 9efgtval 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
) "> >. )
)
10674, 76, 104, 105syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Q ( T `
 ( B `  L ) ) V )  =  ( ( B `  L ) splice  <. Q ,  Q ,  <" V ( M `
 V ) "> >. ) )
10796ffvelrni 5680 . . . . . . . . . . . . . . . 16  |-  ( V  e.  ( I  X.  2o )  ->  ( M `
 V )  e.  ( I  X.  2o ) )
108104, 107syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( M `  V
)  e.  ( I  X.  2o ) )
109104, 108s2cld 11535 . . . . . . . . . . . . . 14  |-  ( ph  ->  <" V ( M `  V ) ">  e. Word  (
I  X.  2o ) )
110 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 ) ) >.
) ) )
11174, 76, 76, 109, 110syl13anc 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 ) ) >.
) ) )
112103, 106, 1113eqtrd 2332 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  B
)  =  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> ) concat  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
11322, 102, 1123eqtr3d 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 )
) >. ) ) )
114113adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( ( 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 )
) >. ) ) )
115 swrdcl 11468 . . . . . . . . . . . . . 14  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o ) )
11638, 115syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o ) )
117116adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  (
( A `  K
) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o ) )
11899adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  <" U
( M `  U
) ">  e. Word  ( I  X.  2o ) )
119 ccatcl 11445 . . . . . . . . . . . 12  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ( M `  U ) ">  e. Word  (
I  X.  2o ) )  ->  ( (
( A `  K
) substr  <. 0 ,  P >. ) concat  <" U ( M `  U ) "> )  e. Word 
( I  X.  2o ) )
120117, 118, 119syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )  e. Word  ( I  X.  2o ) )
121 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )  e. Word  ( I  X.  2o ) )
12238, 121syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  e. Word  ( I  X.  2o ) )
123122adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  Q )  ->  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  e. Word  ( I  X.  2o ) )
124 swrdcl 11468 . . . . . . . . . . . . . 14  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o ) )
12575, 124syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o ) )
126125adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  (
( B `  L
) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o ) )
127109adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  <" V
( M `  V
) ">  e. Word  ( I  X.  2o ) )
128 ccatcl 11445 . . . . . . . . . . . 12  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ( M `  V ) ">  e. Word  (
I  X.  2o ) )  ->  ( (
( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V ( M `  V ) "> )  e. Word 
( I  X.  2o ) )
129126, 127, 128syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )  e. Word  ( I  X.  2o ) )
130 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )  e. Word  ( I  X.  2o ) )
13175, 130syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. )  e. Word  ( I  X.  2o ) )
132131adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  Q )  ->  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
)  e. Word  ( I  X.  2o ) )
133 swrd0len 11471 . . . . . . . . . . . . . . . 16  |-  ( ( ( A `  K
)  e. Word  ( I  X.  2o )  /\  P  e.  ( 0 ... ( # `
 ( A `  K ) ) ) )  ->  ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  =  P )
13438, 39, 133syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  =  P )
135 swrd0len 11471 . . . . . . . . . . . . . . . 16  |-  ( ( ( B `  L
)  e. Word  ( I  X.  2o )  /\  Q  e.  ( 0 ... ( # `
 ( B `  L ) ) ) )  ->  ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  =  Q )
13675, 76, 135syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  =  Q )
137134, 136eqeq12d 2310 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  =  (
# `  ( ( B `  L ) substr  <.
0 ,  Q >. ) )  <->  P  =  Q
) )
138137biimpar 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  Q )  ->  ( # `
 ( ( A `
 K ) substr  <. 0 ,  P >. ) )  =  ( # `  ( ( B `  L ) substr  <. 0 ,  Q >. ) ) )
139 s2len 11553 . . . . . . . . . . . . . . 15  |-  ( # `  <" U ( M `  U ) "> )  =  2
140 s2len 11553 . . . . . . . . . . . . . . 15  |-  ( # `  <" V ( M `  V ) "> )  =  2
141139, 140eqtr4i 2319 . . . . . . . . . . . . . 14  |-  ( # `  <" U ( M `  U ) "> )  =  ( # `  <" V ( M `  V ) "> )
142141a1i 10 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  Q )  ->  ( # `
 <" U ( M `  U ) "> )  =  ( # `  <" V ( M `  V ) "> ) )
143138, 142oveq12d 5892 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  (
( # `  ( ( A `  K ) substr  <. 0 ,  P >. ) )  +  ( # `  <" U ( M `  U ) "> ) )  =  ( ( # `  ( ( B `  L ) substr  <. 0 ,  Q >. ) )  +  ( # `  <" V ( M `  V ) "> ) ) )
144 ccatlen 11446 . . . . . . . . . . . . 13  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ( M `  U ) ">  e. Word  (
I  X.  2o ) )  ->  ( # `  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )
)  =  ( (
# `  ( ( A `  K ) substr  <.
0 ,  P >. ) )  +  ( # `  <" U ( M `  U ) "> ) ) )
145117, 118, 144syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  ( # `
 ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> ) )  =  ( ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  +  (
# `  <" U
( M `  U
) "> )
) )
146 ccatlen 11446 . . . . . . . . . . . . 13  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ( M `  V ) ">  e. Word  (
I  X.  2o ) )  ->  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )
)  =  ( (
# `  ( ( B `  L ) substr  <.
0 ,  Q >. ) )  +  ( # `  <" V ( M `  V ) "> ) ) )
147126, 127, 146syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  Q )  ->  ( # `
 ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) )  =  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  <" V
( M `  V
) "> )
) )
148143, 145, 1473eqtr4d 2338 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  Q )  ->  ( # `
 ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> ) )  =  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )
) )
149 ccatopth 11478 . . . . . . . . . . 11  |-  ( ( ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> )  e. Word  (
I  X.  2o )  /\  ( ( A `
 K ) substr  <. P ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )  /\  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )  e. Word  ( I  X.  2o )  /\  ( ( B `
 L ) substr  <. Q ,  ( # `  ( B `  L )
) >. )  e. Word  (
I  X.  2o ) )  /\  ( # `  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> ) )  =  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )
) )  ->  (
( ( ( ( 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 )
) >. ) )  <->  ( (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> )  /\  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  =  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) ) )
150120, 123, 129, 132, 148, 149syl221anc 1193 . . . . . . . . . 10  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( ( ( 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 )
) >. ) )  <->  ( (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> )  /\  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  =  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
) ) )
151114, 150mpbid 201 . . . . . . . . 9  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )  /\  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. )  =  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
152151simpld 445 . . . . . . . 8  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> ) )
153 ccatopth 11478 . . . . . . . . 9  |-  ( ( ( ( ( A `
 K ) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o )  /\  <" U
( M `  U
) ">  e. Word  ( I  X.  2o ) )  /\  ( ( ( B `  L
) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o )  /\  <" V ( M `
 V ) ">  e. Word  ( I  X.  2o ) )  /\  ( # `  ( ( A `  K ) substr  <. 0 ,  P >. ) )  =  ( # `  ( ( B `  L ) substr  <. 0 ,  Q >. ) ) )  ->  ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U ( M `  U ) "> )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V ( M `
 V ) "> )  <->  ( (
( A `  K
) substr  <. 0 ,  P >. )  =  ( ( B `  L ) substr  <. 0 ,  Q >. )  /\  <" U ( M `  U ) ">  =  <" V ( M `  V ) "> ) ) )
154117, 118, 126, 127, 138, 153syl221anc 1193 . . . . . . . 8  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U ( M `
 U ) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )  <->  ( ( ( A `  K ) substr  <. 0 ,  P >. )  =  ( ( B `  L
) substr  <. 0 ,  Q >. )  /\  <" U
( M `  U
) ">  =  <" V ( M `
 V ) "> ) ) )
155152, 154mpbid 201 . . . . . . 7  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. )  =  ( ( B `  L
) substr  <. 0 ,  Q >. )  /\  <" U
( M `  U
) ">  =  <" V ( M `
 V ) "> ) )
156155simpld 445 . . . . . 6  |-  ( (
ph  /\  P  =  Q )  ->  (
( A `  K
) substr  <. 0 ,  P >. )  =  ( ( B `  L ) substr  <. 0 ,  Q >. ) )
157151simprd 449 . . . . . 6  |-  ( (
ph  /\  P  =  Q )  ->  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  =  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L
) ) >. )
)
158156, 157oveq12d 5892 . . . . 5  |-  ( (
ph  /\  P  =  Q )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) ) )
15991, 158mtand 640 . . . 4  |-  ( ph  ->  -.  P  =  Q )
160159pm2.21d 98 . . 3  |-  ( ph  ->  ( P  =  Q  ->  ( A ` 
0 )  =  ( B `  0 ) ) )
161 uzp1 10277 . . . 4  |-  ( P  e.  ( ZZ>= `  ( Q  +  1 ) )  ->  ( P  =  ( Q  + 
1 )  \/  P  e.  ( ZZ>= `  ( ( Q  +  1 )  +  1 ) ) ) )
16293s1cld 11458 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  <" U ">  e. Word  ( I  X.  2o ) )
163 ccatcl 11445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ">  e. Word  ( I  X.  2o ) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  e. Word  (
I  X.  2o ) )
164116, 162, 163syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> )  e. Word  ( I  X.  2o ) )
16598s1cld 11458 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  <" ( M `
 U ) ">  e. Word  ( I  X.  2o ) )
166 ccatass 11452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> )  e. Word  ( I  X.  2o )  /\  <" ( 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 "> ) concat  <" ( M `
 U ) "> ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )
167164, 165, 122, 166syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( M `  U ) "> ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) ) )
168 ccatass 11452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ">  e. Word  ( I  X.  2o )  /\  <" ( M `  U ) ">  e. Word  ( I  X.  2o ) )  -> 
( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( M `
 U ) "> )  =  ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( <" U "> concat  <" ( M `  U ) "> ) ) )
169116, 162, 165, 168syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( M `
 U ) "> )  =  ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( <" U "> concat  <" ( M `  U ) "> ) ) )
170 df-s2 11514 . . . . . . . . . . . . . . . . . . 19  |-  <" U
( M `  U
) ">  =  ( <" U "> concat 
<" ( M `  U ) "> )
171170oveq2i 5885 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U ( M `  U ) "> )  =  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat 
( <" U "> concat 
<" ( M `  U ) "> ) )
172169, 171syl6eqr 2346 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( M `
 U ) "> )  =  ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U
( M `  U
) "> )
)
173172oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( 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 )
) >. ) ) )
174104s1cld 11458 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  <" V ">  e. Word  ( I  X.  2o ) )
175108s1cld 11458 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  <" ( M `
 V ) ">  e. Word  ( I  X.  2o ) )
176 ccatass 11452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ">  e. Word  ( I  X.  2o )  /\  <" ( M `  V ) ">  e. Word  ( I  X.  2o ) )  -> 
( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V "> concat  <" ( M `  V ) "> ) ) )
177125, 174, 175, 176syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V "> concat  <" ( M `  V ) "> ) ) )
178 df-s2 11514 . . . . . . . . . . . . . . . . . . 19  |-  <" V
( M `  V
) ">  =  ( <" V "> concat 
<" ( M `  V ) "> )
179178oveq2i 5885 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V ( M `  V ) "> )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( <" V "> concat 
<" ( M `  V ) "> ) )
180177, 179syl6eqr 2346 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V
( M `  V
) "> )
)
181180oveq1d 5889 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( 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 )
) >. ) ) )
182113, 173, 1813eqtr4d 2338 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  <" ( M `  U ) "> ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
183167, 182eqtr3d 2330 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
184183adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
185164adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  e. Word  (
I  X.  2o ) )
186165adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" ( M `  U ) ">  e. Word  ( I  X.  2o ) )
187122adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  e. Word  ( I  X.  2o ) )
188 ccatcl 11445 . . . . . . . . . . . . . . 15  |-  ( (
<" ( M `  U ) ">  e. Word  ( I  X.  2o )  /\  ( ( A `
 K ) substr  <. P ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )  ->  ( <" ( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
)  e. Word  ( I  X.  2o ) )
189186, 187, 188syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  e. Word  (
I  X.  2o ) )
190 ccatcl 11445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ">  e. Word  ( I  X.  2o ) )  ->  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  (
I  X.  2o ) )
191125, 174, 190syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  ( I  X.  2o ) )
192191adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  (
I  X.  2o ) )
193175adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" ( M `  V ) ">  e. Word  ( I  X.  2o ) )
194 ccatcl 11445 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  ( I  X.  2o )  /\  <" ( M `  V
) ">  e. Word  ( I  X.  2o ) )  ->  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> )  e. Word  (
I  X.  2o ) )
195192, 193, 194syl2anc 642 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  e. Word  (
I  X.  2o ) )
196131adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
)  e. Word  ( I  X.  2o ) )
197 ccatlen 11446 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ">  e. Word  ( I  X.  2o ) )  ->  ( # `
 ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  =  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  <" V "> ) ) )
198125, 174, 197syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  =  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  <" V "> ) ) )
199 s1len 11460 . . . . . . . . . . . . . . . . . . . . 21  |-  ( # `  <" V "> )  =  1
200199a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( # `  <" V "> )  =  1 )
201136, 200oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( # `  (
( B `  L
) substr  <. 0 ,  Q >. ) )  +  (
# `  <" V "> ) )  =  ( Q  +  1 ) )
202198, 201eqtrd 2328 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  =  ( Q  +  1 ) )
203134, 202eqeq12d 2310 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  =  (
# `  ( (
( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  <->  P  =  ( Q  +  1
) ) )
204203biimpar 471 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( # `
 ( ( A `
 K ) substr  <. 0 ,  P >. ) )  =  ( # `  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) ) )
205 s1len 11460 . . . . . . . . . . . . . . . . . 18  |-  ( # `  <" U "> )  =  1
206 s1len 11460 . . . . . . . . . . . . . . . . . 18  |-  ( # `  <" ( M `
 V ) "> )  =  1
207205, 206eqtr4i 2319 . . . . . . . . . . . . . . . . 17  |-  ( # `  <" U "> )  =  ( # `
 <" ( M `
 V ) "> )
208207a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( # `
 <" U "> )  =  ( # `
 <" ( M `
 V ) "> ) )
209204, 208oveq12d 5892 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( # `  ( ( A `  K ) substr  <. 0 ,  P >. ) )  +  ( # `  <" U "> ) )  =  ( ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  +  ( # `  <" ( M `  V
) "> )
) )
210116adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( A `  K
) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o ) )
211162adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" U ">  e. Word  ( I  X.  2o ) )
212 ccatlen 11446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( A `  K ) substr  <. 0 ,  P >. )  e. Word  (
I  X.  2o )  /\  <" U ">  e. Word  ( I  X.  2o ) )  ->  ( # `
 ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) )  =  ( ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  +  (
# `  <" U "> ) ) )
213210, 211, 212syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( # `
 ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) )  =  ( ( # `  (
( A `  K
) substr  <. 0 ,  P >. ) )  +  (
# `  <" U "> ) ) )
214 ccatlen 11446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  ( I  X.  2o )  /\  <" ( M `  V
) ">  e. Word  ( I  X.  2o ) )  ->  ( # `  (
( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> ) )  =  ( ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  +  ( # `  <" ( M `  V
) "> )
) )
215192, 193, 214syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( # `
 ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) )  =  ( ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) )  +  ( # `  <" ( M `  V
) "> )
) )
216209, 213, 2153eqtr4d 2338 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( # `
 ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) )  =  (
# `  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) ) )
217 ccatopth 11478 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  e. Word  ( I  X.  2o )  /\  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  e. Word  (
I  X.  2o ) )  /\  ( ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  e. Word  (
I  X.  2o )  /\  ( ( B `
 L ) substr  <. Q ,  ( # `  ( B `  L )
) >. )  e. Word  (
I  X.  2o ) )  /\  ( # `  ( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> ) )  =  (
# `  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) ) )  ->  ( ( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U
) "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
) )  =  ( ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  <->  ( (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  =  ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  /\  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) ) )
218185, 189, 195, 196, 216, 217syl221anc 1193 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> ) concat  ( <" ( M `  U ) "> concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )  =  ( ( ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) )  <->  ( (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  =  ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  /\  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) ) )
219184, 218mpbid 201 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> )  =  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> )  /\  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) ) )
220219simpld 445 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  <" U "> )  =  ( ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> ) )
221 ccatopth 11478 . . . . . . . . . . . 12  |-  ( ( ( ( ( A `
 K ) substr  <. 0 ,  P >. )  e. Word  ( I  X.  2o )  /\  <" U ">  e. Word  ( I  X.  2o ) )  /\  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  e. Word  ( I  X.  2o )  /\  <" ( M `  V
) ">  e. Word  ( I  X.  2o ) )  /\  ( # `  ( ( A `  K ) substr  <. 0 ,  P >. ) )  =  ( # `  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) ) )  ->  ( ( ( ( A `  K
) substr  <. 0 ,  P >. ) concat  <" U "> )  =  (
( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `
 V ) "> )  <->  ( (
( A `  K
) substr  <. 0 ,  P >. )  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> )  /\  <" U ">  =  <" ( M `  V ) "> ) ) )
222210, 211, 192, 193, 204, 221syl221anc 1193 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( A `
 K ) substr  <. 0 ,  P >. ) concat  <" U "> )  =  ( (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  <" ( M `  V ) "> )  <->  ( (
( A `  K
) substr  <. 0 ,  P >. )  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> )  /\  <" U ">  =  <" ( M `  V ) "> ) ) )
223220, 222mpbid 201 . . . . . . . . . 10  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> )  /\  <" U ">  =  <" ( M `  V ) "> ) )
224223simpld 445 . . . . . . . . 9  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( A `  K
) substr  <. 0 ,  P >. )  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  <" V "> ) )
225224oveq1d 5889 . . . . . . . 8  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) ) )
226125adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( B `  L
) substr  <. 0 ,  Q >. )  e. Word  ( I  X.  2o ) )
227174adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" V ">  e. Word  ( I  X.  2o ) )
228 ccatass 11452 . . . . . . . . 9  |-  ( ( ( ( B `  L ) substr  <. 0 ,  Q >. )  e. Word  (
I  X.  2o )  /\  <" V ">  e. Word  ( I  X.  2o )  /\  (
( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
)  e. Word  ( I  X.  2o ) )  -> 
( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
) ) )
229226, 227, 187, 228syl3anc 1182 . . . . . . . 8  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat  <" V "> ) concat  ( ( A `  K ) substr  <. P , 
( # `  ( A `
 K ) )
>. ) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
) ) )
230223simprd 449 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" U ">  =  <" ( M `  V ) "> )
231 s111 11464 . . . . . . . . . . . . . . . . 17  |-  ( ( U  e.  ( I  X.  2o )  /\  ( M `  V )  e.  ( I  X.  2o ) )  ->  ( <" U ">  =  <" ( M `
 V ) ">  <->  U  =  ( M `  V )
) )
23293, 108, 231syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( <" U ">  =  <" ( M `  V ) ">  <->  U  =  ( M `  V )
) )
233232adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( <" U ">  =  <" ( M `
 V ) ">  <->  U  =  ( M `  V )
) )
234230, 233mpbid 201 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  U  =  ( M `  V ) )
235234fveq2d 5545 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( M `  U )  =  ( M `  ( M `  V ) ) )
2368efgmnvl 15039 . . . . . . . . . . . . . . 15  |-  ( V  e.  ( I  X.  2o )  ->  ( M `
 ( M `  V ) )  =  V )
237104, 236syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( M `  ( M `  V )
)  =  V )
238237adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( M `  ( M `  V ) )  =  V )
239235, 238eqtrd 2328 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( M `  U )  =  V )
240239s1eqd 11456 . . . . . . . . . . 11  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  <" ( M `  U ) ">  =  <" V "> )
241240oveq1d 5889 . . . . . . . . . 10  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  (
<" V "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) ) )
242219simprd 449 . . . . . . . . . 10  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( <" ( M `  U ) "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) )
243241, 242eqtr3d 2330 . . . . . . . . 9  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  ( <" V "> concat  ( ( A `  K
) substr  <. P ,  (
# `  ( A `  K ) ) >.
) )  =  ( ( B `  L
) substr  <. Q ,  (
# `  ( B `  L ) ) >.
) )
244243oveq2d 5890 . . . . . . . 8  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( <" V "> concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K
) ) >. )
) )  =  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( B `  L ) substr  <. Q ,  ( # `  ( B `  L )
) >. ) ) )
245225, 229, 2443eqtrd 2332 . . . . . . 7  |-  ( (
ph  /\  P  =  ( Q  +  1
) )  ->  (
( ( A `  K ) substr  <. 0 ,  P >. ) concat  ( ( A `  K ) substr  <. P ,  ( # `  ( A `  K )
) >. ) )  =  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( B `  L ) substr  <. Q , 
( # `  ( B `
 L ) )
>. ) ) )
24691, 245mtand 640 . . . . . 6  |-  ( ph  ->  -.  P  =  ( Q  +  1 ) )
247246pm2.21d 98 . . . . 5  |-  ( ph  ->  ( P  =  ( Q  +  1 )  ->  ( A ` 
0 )  =  ( B `  0 ) ) )
248 elfzelz 10814 . . . . . . . . . . . 12  |-  ( Q  e.  ( 0 ... ( # `  ( B `  L )
) )  ->  Q  e.  ZZ )
24976, 248syl 15 . . . . . . . . . . 11  |-  ( ph  ->  Q  e.  ZZ )
250249zcnd 10134 . . . . . . . . . 10  |-  ( ph  ->  Q  e.  CC )
251 ax-1cn 8811 . . . . . . . . . . 11  |-  1  e.  CC
252251a1i 10 . . . . . . . . . 10  |-  ( ph  ->  1  e.  CC )
253250, 252, 252addassd 8873 . . . . . . . . 9  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  =  ( Q  +  ( 1  +  1 ) ) )
254 df-2 9820 . . . . . . . . . 10  |-  2  =  ( 1  +  1 )
255254oveq2i 5885 . . . . . . . . 9  |-  ( Q  +  2 )  =  ( Q  +  ( 1  +  1 ) )
256253, 255syl6eqr 2346 . . . . . . . 8  |-  ( ph  ->  ( ( Q  + 
1 )  +  1 )  =  ( Q  +  2 ) )
257256fveq2d 5545 . . . . . . 7  |-  ( ph  ->  ( ZZ>= `  ( ( Q  +  1 )  +  1 ) )  =  ( ZZ>= `  ( Q  +  2 ) ) )
258257eleq2d 2363 . . . . . 6  |-  ( ph  ->  ( P  e.  (
ZZ>= `  ( ( Q  +  1 )  +  1 ) )  <->  P  e.  ( ZZ>= `  ( Q  +  2 ) ) ) )
2593, 7, 8, 9, 10, 11efgsfo 15064 . . . . . . . . . 10  |-  S : dom  S -onto-> W
260 swrdcl 11468 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )  e. Word  ( I  X.  2o ) )
26138, 260syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. )  e. Word  (
I  X.  2o ) )
262 ccatcl 11445 . . . . . . . . . . . 12  |-  ( ( ( ( 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 )
) >. ) )  e. Word 
( I  X.  2o ) )
263125, 261, 262syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  e. Word 
( I  X.  2o ) )
2643efgrcl 15040 . . . . . . . . . . . . 13  |-  ( ( A `  K )  e.  W  ->  (
I  e.  _V  /\  W  = Word  ( I  X.  2o ) ) )
26537, 264syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( I  e.  _V  /\  W  = Word  ( I  X.  2o ) ) )
266265simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  W  = Word  ( I  X.  2o ) )
267263, 266eleqtrrd 2373 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  e.  W )
268 foelrn 5695 . . . . . . . . . 10  |-  ( ( S : dom  S -onto-> W  /\  ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  e.  W )  ->  E. c  e.  dom  S ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) )
269259, 267, 268sylancr 644 . . . . . . . . 9  |-  ( ph  ->  E. c  e.  dom  S ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) )
270269adantr 451 . . . . . . . 8  |-  ( (
ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  ->  E. c  e.  dom  S ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) )
27120ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  A. a  e.  dom  S A. b  e.  dom  S ( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  ->  ( ( S `  a )  =  ( S `  b )  ->  (
a `  0 )  =  ( b ` 
0 ) ) ) )
2726ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  A  e.  dom  S )
27321ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  B  e.  dom  S )
27422ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( S `  A
)  =  ( S `
 B ) )
27523ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  -.  ( A `  0
)  =  ( B `
 0 ) )
27639ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  P  e.  ( 0 ... ( # `  ( A `  K )
) ) )
27776ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  Q  e.  ( 0 ... ( # `  ( B `  L )
) ) )
27893ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  U  e.  ( I  X.  2o ) )
279104ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  V  e.  ( I  X.  2o ) )
28092ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( S `  A
)  =  ( P ( T `  ( A `  K )
) U ) )
281103ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( S `  B
)  =  ( Q ( T `  ( B `  L )
) V ) )
2822ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  -.  ( A `  K
)  =  ( B `
 L ) )
283 simplr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  ->  P  e.  ( ZZ>= `  ( Q  +  2
) ) )
284 simprl 732 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
c  e.  dom  S
)
285 simprr 733 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) )
286285eqcomd 2301 . . . . . . . . . . 11  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( S `  c
)  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
2873, 7, 8, 9, 10, 11, 271, 272, 273, 274, 275, 19, 61, 276, 277, 278, 279, 280, 281, 282, 283, 284, 286efgredlemd 15069 . . . . . . . . . 10  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  ( c  e.  dom  S  /\  ( ( ( B `
 L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
) ) )  -> 
( A `  0
)  =  ( B `
 0 ) )
288287expr 598 . . . . . . . . 9  |-  ( ( ( ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  /\  c  e. 
dom  S )  -> 
( ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat 
( ( A `  K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) )  =  ( S `  c
)  ->  ( A `  0 )  =  ( B `  0
) ) )
289288rexlimdva 2680 . . . . . . . 8  |-  ( (
ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  ->  ( E. c  e.  dom  S ( ( ( B `  L ) substr  <. 0 ,  Q >. ) concat  ( ( A `  K ) substr  <.
( Q  +  2 ) ,  ( # `  ( A `  K
) ) >. )
)  =  ( S `
 c )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
290270, 289mpd 14 . . . . . . 7  |-  ( (
ph  /\  P  e.  ( ZZ>= `  ( Q  +  2 ) ) )  ->  ( A `  0 )  =  ( B `  0
) )
291290ex 423 . . . . . 6  |-  ( ph  ->  ( P  e.  (
ZZ>= `  ( Q  + 
2 ) )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
292258, 291sylbid 206 . . . . 5  |-  ( ph  ->  ( P  e.  (
ZZ>= `  ( ( Q  +  1 )  +  1 ) )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
293247, 292jaod 369 . . . 4  |-  ( ph  ->  ( ( P  =  ( Q  +  1 )  \/  P  e.  ( ZZ>= `  ( ( Q  +  1 )  +  1 ) ) )  ->  ( A `  0 )  =  ( B `  0
) ) )
294161, 293syl5 28 . . 3  |-  ( ph  ->  ( P  e.  (
ZZ>= `  ( Q  + 
1 ) )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
295160, 294jaod 369 . 2  |-  ( ph  ->  ( ( P  =  Q  \/  P  e.  ( ZZ>= `  ( Q  +  1 ) ) )  ->  ( A `  0 )  =  ( B `  0
) ) )
2961, 295syl5 28 1  |-  ( ph  ->  ( P  e.  (
ZZ>= `  Q )  -> 
( A `  0
)  =  ( B `
 0 ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1632    e. wcel 1696   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    \ cdif 3162   (/)c0 3468   {csn 3653   <.cop 3656   <.cotp 3657   U_ciun 3921   class class class wbr 4039    e. cmpt 4093    _I cid 4320    X. cxp 4703   dom cdm 4705   ran crn 4706   -->wf 5267   -onto->wfo 5269   ` cfv 5271  (class class class)co 5874    e. cmpt2 5876   1oc1o 6488   2oc2o 6489   CCcc 8751   0cc0 8753   1c1 8754    + caddc 8756    < clt 8883    - cmin 9053   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   ...cfz 10798  ..^cfzo 10886   #chash 11353  Word cword 11419   concat cconcat 11420   <"cs1 11421   substr csubstr 11422   splice csplice 11423   <"cs2 11507   ~FG cefg 15031
This theorem is referenced by:  efgredlemb  15071
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-ot 3663  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-2o 6496  df-oadd 6499  df-er 6676  df-map 6790  df-pm 6791  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-nn 9763  df-2 9820  df-n0 9982  df-z 10041  df-uz 10247  df-rp 10371  df-fz 10799  df-fzo 10887  df-hash 11354  df-word 11425  df-concat 11426  df-s1 11427  df-substr 11428  df-splice 11429  df-s2 11514
  Copyright terms: Public domain W3C validator