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

Theorem efgredlemd 15069
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 ) )
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
efgredlemd  |-  ( ph  ->  ( 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    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 efgredlemd
Dummy variable  i is distinct from all other variables.
StepHypRef Expression
1 efgredlemd.c . . . . . . 7  |-  ( 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, 7efgsdm 15055 . . . . . . . 8  |-  ( C  e.  dom  S  <->  ( C  e.  (Word  W  \  { (/)
} )  /\  ( C `  0 )  e.  D  /\  A. i  e.  ( 1..^ ( # `  C ) ) ( C `  i )  e.  ran  ( T `
 ( C `  ( i  -  1 ) ) ) ) )
98simp1bi 970 . . . . . . 7  |-  ( C  e.  dom  S  ->  C  e.  (Word  W  \  { (/) } ) )
101, 9syl 15 . . . . . 6  |-  ( ph  ->  C  e.  (Word  W  \  { (/) } ) )
11 eldifi 3311 . . . . . 6  |-  ( C  e.  (Word  W  \  { (/) } )  ->  C  e. Word  W )
1210, 11syl 15 . . . . 5  |-  ( ph  ->  C  e. Word  W )
13 efgredlem.2 . . . . . . . . . 10  |-  ( ph  ->  A  e.  dom  S
)
142, 3, 4, 5, 6, 7efgsdm 15055 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
1514simp1bi 970 . . . . . . . . . 10  |-  ( A  e.  dom  S  ->  A  e.  (Word  W  \  { (/) } ) )
1613, 15syl 15 . . . . . . . . 9  |-  ( ph  ->  A  e.  (Word  W  \  { (/) } ) )
17 eldifi 3311 . . . . . . . . 9  |-  ( A  e.  (Word  W  \  { (/) } )  ->  A  e. Word  W )
1816, 17syl 15 . . . . . . . 8  |-  ( ph  ->  A  e. Word  W )
19 wrdf 11435 . . . . . . . 8  |-  ( A  e. Word  W  ->  A : ( 0..^ (
# `  A )
) --> W )
2018, 19syl 15 . . . . . . 7  |-  ( ph  ->  A : ( 0..^ ( # `  A
) ) --> W )
21 fzossfz 10908 . . . . . . . . 9  |-  ( 0..^ ( ( # `  A
)  -  1 ) )  C_  ( 0 ... ( ( # `  A )  -  1 ) )
22 lencl 11437 . . . . . . . . . . . 12  |-  ( A  e. Word  W  ->  ( # `
 A )  e. 
NN0 )
2318, 22syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  A
)  e.  NN0 )
2423nn0zd 10131 . . . . . . . . . 10  |-  ( ph  ->  ( # `  A
)  e.  ZZ )
25 fzoval 10892 . . . . . . . . . 10  |-  ( (
# `  A )  e.  ZZ  ->  ( 0..^ ( # `  A
) )  =  ( 0 ... ( (
# `  A )  -  1 ) ) )
2624, 25syl 15 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( # `  A ) )  =  ( 0 ... (
( # `  A )  -  1 ) ) )
2721, 26syl5sseqr 3240 . . . . . . . 8  |-  ( ph  ->  ( 0..^ ( (
# `  A )  -  1 ) ) 
C_  ( 0..^ (
# `  A )
) )
28 efgredlemb.k . . . . . . . . 9  |-  K  =  ( ( ( # `  A )  -  1 )  -  1 )
29 efgredlem.1 . . . . . . . . . . . 12  |-  ( ph  ->  A. a  e.  dom  S A. b  e.  dom  S ( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  ->  ( ( S `  a )  =  ( S `  b )  ->  (
a `  0 )  =  ( b ` 
0 ) ) ) )
30 efgredlem.3 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  dom  S
)
31 efgredlem.4 . . . . . . . . . . . 12  |-  ( ph  ->  ( S `  A
)  =  ( S `
 B ) )
32 efgredlem.5 . . . . . . . . . . . 12  |-  ( ph  ->  -.  ( A ` 
0 )  =  ( B `  0 ) )
332, 3, 4, 5, 6, 7, 29, 13, 30, 31, 32efgredlema 15065 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( # `  A )  -  1 )  e.  NN  /\  ( ( # `  B
)  -  1 )  e.  NN ) )
3433simpld 445 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  A
)  -  1 )  e.  NN )
35 fzo0end 10931 . . . . . . . . . 10  |-  ( ( ( # `  A
)  -  1 )  e.  NN  ->  (
( ( # `  A
)  -  1 )  -  1 )  e.  ( 0..^ ( (
# `  A )  -  1 ) ) )
3634, 35syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( ( # `  A )  -  1 )  -  1 )  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )
3728, 36syl5eqel 2380 . . . . . . . 8  |-  ( ph  ->  K  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )
3827, 37sseldd 3194 . . . . . . 7  |-  ( ph  ->  K  e.  ( 0..^ ( # `  A
) ) )
39 ffvelrn 5679 . . . . . . 7  |-  ( ( A : ( 0..^ ( # `  A
) ) --> W  /\  K  e.  ( 0..^ ( # `  A
) ) )  -> 
( A `  K
)  e.  W )
4020, 38, 39syl2anc 642 . . . . . 6  |-  ( ph  ->  ( A `  K
)  e.  W )
4140s1cld 11458 . . . . 5  |-  ( ph  ->  <" ( A `
 K ) ">  e. Word  W )
42 eldifsn 3762 . . . . . . . 8  |-  ( C  e.  (Word  W  \  { (/) } )  <->  ( C  e. Word  W  /\  C  =/=  (/) ) )
43 lennncl 11438 . . . . . . . 8  |-  ( ( C  e. Word  W  /\  C  =/=  (/) )  ->  ( # `
 C )  e.  NN )
4442, 43sylbi 187 . . . . . . 7  |-  ( C  e.  (Word  W  \  { (/) } )  -> 
( # `  C )  e.  NN )
4510, 44syl 15 . . . . . 6  |-  ( ph  ->  ( # `  C
)  e.  NN )
46 lbfzo0 10919 . . . . . 6  |-  ( 0  e.  ( 0..^ (
# `  C )
)  <->  ( # `  C
)  e.  NN )
4745, 46sylibr 203 . . . . 5  |-  ( ph  ->  0  e.  ( 0..^ ( # `  C
) ) )
48 ccatval1 11447 . . . . 5  |-  ( ( C  e. Word  W  /\  <" ( A `  K ) ">  e. Word  W  /\  0  e.  ( 0..^ ( # `  C ) ) )  ->  ( ( C concat  <" ( A `  K ) "> ) `  0 )  =  ( C ` 
0 ) )
4912, 41, 47, 48syl3anc 1182 . . . 4  |-  ( ph  ->  ( ( C concat  <" ( A `  K ) "> ) `  0
)  =  ( C `
 0 ) )
502, 3, 4, 5, 6, 7efgsdm 15055 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
5150simp1bi 970 . . . . . . . . . 10  |-  ( B  e.  dom  S  ->  B  e.  (Word  W  \  { (/) } ) )
5230, 51syl 15 . . . . . . . . 9  |-  ( ph  ->  B  e.  (Word  W  \  { (/) } ) )
53 eldifi 3311 . . . . . . . . 9  |-  ( B  e.  (Word  W  \  { (/) } )  ->  B  e. Word  W )
5452, 53syl 15 . . . . . . . 8  |-  ( ph  ->  B  e. Word  W )
55 wrdf 11435 . . . . . . . 8  |-  ( B  e. Word  W  ->  B : ( 0..^ (
# `  B )
) --> W )
5654, 55syl 15 . . . . . . 7  |-  ( ph  ->  B : ( 0..^ ( # `  B
) ) --> W )
57 fzossfz 10908 . . . . . . . . 9  |-  ( 0..^ ( ( # `  B
)  -  1 ) )  C_  ( 0 ... ( ( # `  B )  -  1 ) )
58 lencl 11437 . . . . . . . . . . . 12  |-  ( B  e. Word  W  ->  ( # `
 B )  e. 
NN0 )
5954, 58syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  B
)  e.  NN0 )
6059nn0zd 10131 . . . . . . . . . 10  |-  ( ph  ->  ( # `  B
)  e.  ZZ )
61 fzoval 10892 . . . . . . . . . 10  |-  ( (
# `  B )  e.  ZZ  ->  ( 0..^ ( # `  B
) )  =  ( 0 ... ( (
# `  B )  -  1 ) ) )
6260, 61syl 15 . . . . . . . . 9  |-  ( ph  ->  ( 0..^ ( # `  B ) )  =  ( 0 ... (
( # `  B )  -  1 ) ) )
6357, 62syl5sseqr 3240 . . . . . . . 8  |-  ( ph  ->  ( 0..^ ( (
# `  B )  -  1 ) ) 
C_  ( 0..^ (
# `  B )
) )
64 efgredlemb.l . . . . . . . . 9  |-  L  =  ( ( ( # `  B )  -  1 )  -  1 )
6533simprd 449 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  B
)  -  1 )  e.  NN )
66 fzo0end 10931 . . . . . . . . . 10  |-  ( ( ( # `  B
)  -  1 )  e.  NN  ->  (
( ( # `  B
)  -  1 )  -  1 )  e.  ( 0..^ ( (
# `  B )  -  1 ) ) )
6765, 66syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( ( # `  B )  -  1 )  -  1 )  e.  ( 0..^ ( ( # `  B
)  -  1 ) ) )
6864, 67syl5eqel 2380 . . . . . . . 8  |-  ( ph  ->  L  e.  ( 0..^ ( ( # `  B
)  -  1 ) ) )
6963, 68sseldd 3194 . . . . . . 7  |-  ( ph  ->  L  e.  ( 0..^ ( # `  B
) ) )
70 ffvelrn 5679 . . . . . . 7  |-  ( ( B : ( 0..^ ( # `  B
) ) --> W  /\  L  e.  ( 0..^ ( # `  B
) ) )  -> 
( B `  L
)  e.  W )
7156, 69, 70syl2anc 642 . . . . . 6  |-  ( ph  ->  ( B `  L
)  e.  W )
7271s1cld 11458 . . . . 5  |-  ( ph  ->  <" ( B `
 L ) ">  e. Word  W )
73 ccatval1 11447 . . . . 5  |-  ( ( C  e. Word  W  /\  <" ( B `  L ) ">  e. Word  W  /\  0  e.  ( 0..^ ( # `  C ) ) )  ->  ( ( C concat  <" ( B `  L ) "> ) `  0 )  =  ( C ` 
0 ) )
7412, 72, 47, 73syl3anc 1182 . . . 4  |-  ( ph  ->  ( ( C concat  <" ( B `  L ) "> ) `  0
)  =  ( C `
 0 ) )
7549, 74eqtr4d 2331 . . 3  |-  ( ph  ->  ( ( C concat  <" ( A `  K ) "> ) `  0
)  =  ( ( C concat  <" ( B `
 L ) "> ) `  0
) )
76 fviss 5596 . . . . . . . . . 10  |-  (  _I 
` Word  ( I  X.  2o ) )  C_ Word  ( I  X.  2o )
772, 76eqsstri 3221 . . . . . . . . 9  |-  W  C_ Word  ( I  X.  2o )
7877, 40sseldi 3191 . . . . . . . 8  |-  ( ph  ->  ( A `  K
)  e. Word  ( I  X.  2o ) )
79 lencl 11437 . . . . . . . 8  |-  ( ( A `  K )  e. Word  ( I  X.  2o )  ->  ( # `  ( A `  K
) )  e.  NN0 )
8078, 79syl 15 . . . . . . 7  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  NN0 )
8180nn0red 10035 . . . . . 6  |-  ( ph  ->  ( # `  ( A `  K )
)  e.  RR )
82 2rp 10375 . . . . . 6  |-  2  e.  RR+
83 ltaddrp 10402 . . . . . 6  |-  ( ( ( # `  ( A `  K )
)  e.  RR  /\  2  e.  RR+ )  -> 
( # `  ( A `
 K ) )  <  ( ( # `  ( A `  K
) )  +  2 ) )
8481, 82, 83sylancl 643 . . . . 5  |-  ( ph  ->  ( # `  ( A `  K )
)  <  ( ( # `
 ( A `  K ) )  +  2 ) )
8523nn0red 10035 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  A
)  e.  RR )
8685lem1d 9706 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  A
)  -  1 )  <_  ( # `  A
) )
87 fznn 10868 . . . . . . . . . . 11  |-  ( (
# `  A )  e.  ZZ  ->  ( (
( # `  A )  -  1 )  e.  ( 1 ... ( # `
 A ) )  <-> 
( ( ( # `  A )  -  1 )  e.  NN  /\  ( ( # `  A
)  -  1 )  <_  ( # `  A
) ) ) )
8824, 87syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( # `  A )  -  1 )  e.  ( 1 ... ( # `  A
) )  <->  ( (
( # `  A )  -  1 )  e.  NN  /\  ( (
# `  A )  -  1 )  <_ 
( # `  A ) ) ) )
8934, 86, 88mpbir2and 888 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  A
)  -  1 )  e.  ( 1 ... ( # `  A
) ) )
902, 3, 4, 5, 6, 7efgsres 15063 . . . . . . . . 9  |-  ( ( A  e.  dom  S  /\  ( ( # `  A
)  -  1 )  e.  ( 1 ... ( # `  A
) ) )  -> 
( A  |`  (
0..^ ( ( # `  A )  -  1 ) ) )  e. 
dom  S )
9113, 89, 90syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( A  |`  (
0..^ ( ( # `  A )  -  1 ) ) )  e. 
dom  S )
922, 3, 4, 5, 6, 7efgsval 15056 . . . . . . . 8  |-  ( ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) )  e.  dom  S  ->  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) `  ( ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  - 
1 ) ) )
9391, 92syl 15 . . . . . . 7  |-  ( ph  ->  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) `  ( ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  - 
1 ) ) )
94 1nn0 9997 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
95 nn0uz 10278 . . . . . . . . . . . . . . . 16  |-  NN0  =  ( ZZ>= `  0 )
9694, 95eleqtri 2368 . . . . . . . . . . . . . . 15  |-  1  e.  ( ZZ>= `  0 )
97 fzss1 10846 . . . . . . . . . . . . . . 15  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... ( # `  A
) )  C_  (
0 ... ( # `  A
) ) )
9896, 97ax-mp 8 . . . . . . . . . . . . . 14  |-  ( 1 ... ( # `  A
) )  C_  (
0 ... ( # `  A
) )
9998, 89sseldi 3191 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( # `  A
)  -  1 )  e.  ( 0 ... ( # `  A
) ) )
100 swrd0val 11470 . . . . . . . . . . . . 13  |-  ( ( A  e. Word  W  /\  ( ( # `  A
)  -  1 )  e.  ( 0 ... ( # `  A
) ) )  -> 
( A substr  <. 0 ,  ( ( # `  A
)  -  1 )
>. )  =  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )
10118, 99, 100syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( A substr  <. 0 ,  ( ( # `  A )  -  1 ) >. )  =  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )
102101fveq2d 5545 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( A substr  <. 0 ,  ( ( # `  A
)  -  1 )
>. ) )  =  (
# `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )
103 swrd0len 11471 . . . . . . . . . . . 12  |-  ( ( A  e. Word  W  /\  ( ( # `  A
)  -  1 )  e.  ( 0 ... ( # `  A
) ) )  -> 
( # `  ( A substr  <. 0 ,  ( (
# `  A )  -  1 ) >.
) )  =  ( ( # `  A
)  -  1 ) )
10418, 99, 103syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( A substr  <. 0 ,  ( ( # `  A
)  -  1 )
>. ) )  =  ( ( # `  A
)  -  1 ) )
105102, 104eqtr3d 2330 . . . . . . . . . 10  |-  ( ph  ->  ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( ( # `  A
)  -  1 ) )
106105oveq1d 5889 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  - 
1 )  =  ( ( ( # `  A
)  -  1 )  -  1 ) )
107106, 28syl6eqr 2346 . . . . . . . 8  |-  ( ph  ->  ( ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  - 
1 )  =  K )
108107fveq2d 5545 . . . . . . 7  |-  ( ph  ->  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) `  ( ( # `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  - 
1 ) )  =  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) `  K ) )
109 fvres 5558 . . . . . . . 8  |-  ( K  e.  ( 0..^ ( ( # `  A
)  -  1 ) )  ->  ( ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) `  K
)  =  ( A `
 K ) )
11037, 109syl 15 . . . . . . 7  |-  ( ph  ->  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) `  K )  =  ( A `  K ) )
11193, 108, 1103eqtrd 2332 . . . . . 6  |-  ( ph  ->  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( A `  K
) )
112111fveq2d 5545 . . . . 5  |-  ( ph  ->  ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )  =  ( # `  ( A `  K )
) )
1132, 3, 4, 5, 6, 7efgsdmi 15057 . . . . . . . 8  |-  ( ( A  e.  dom  S  /\  ( ( # `  A
)  -  1 )  e.  NN )  -> 
( S `  A
)  e.  ran  ( T `  ( A `  ( ( ( # `  A )  -  1 )  -  1 ) ) ) )
11413, 34, 113syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( S `  A
)  e.  ran  ( T `  ( A `  ( ( ( # `  A )  -  1 )  -  1 ) ) ) )
11528fveq2i 5544 . . . . . . . . 9  |-  ( A `
 K )  =  ( A `  (
( ( # `  A
)  -  1 )  -  1 ) )
116115fveq2i 5544 . . . . . . . 8  |-  ( T `
 ( A `  K ) )  =  ( T `  ( A `  ( (
( # `  A )  -  1 )  - 
1 ) ) )
117116rneqi 4921 . . . . . . 7  |-  ran  ( T `  ( A `  K ) )  =  ran  ( T `  ( A `  ( ( ( # `  A
)  -  1 )  -  1 ) ) )
118114, 117syl6eleqr 2387 . . . . . 6  |-  ( ph  ->  ( S `  A
)  e.  ran  ( T `  ( A `  K ) ) )
1192, 3, 4, 5efgtlen 15051 . . . . . 6  |-  ( ( ( A `  K
)  e.  W  /\  ( S `  A )  e.  ran  ( T `
 ( A `  K ) ) )  ->  ( # `  ( S `  A )
)  =  ( (
# `  ( A `  K ) )  +  2 ) )
12040, 118, 119syl2anc 642 . . . . 5  |-  ( ph  ->  ( # `  ( S `  A )
)  =  ( (
# `  ( A `  K ) )  +  2 ) )
12184, 112, 1203brtr4d 4069 . . . 4  |-  ( ph  ->  ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) ) )
122 efgredlemb.p . . . . . . . . 9  |-  ( ph  ->  P  e.  ( 0 ... ( # `  ( A `  K )
) ) )
123 efgredlemb.q . . . . . . . . 9  |-  ( ph  ->  Q  e.  ( 0 ... ( # `  ( B `  L )
) ) )
124 efgredlemb.u . . . . . . . . 9  |-  ( ph  ->  U  e.  ( I  X.  2o ) )
125 efgredlemb.v . . . . . . . . 9  |-  ( ph  ->  V  e.  ( I  X.  2o ) )
126 efgredlemb.6 . . . . . . . . 9  |-  ( ph  ->  ( S `  A
)  =  ( P ( T `  ( A `  K )
) U ) )
127 efgredlemb.7 . . . . . . . . 9  |-  ( ph  ->  ( S `  B
)  =  ( Q ( T `  ( B `  L )
) V ) )
128 efgredlemb.8 . . . . . . . . 9  |-  ( ph  ->  -.  ( A `  K )  =  ( B `  L ) )
129 efgredlemd.9 . . . . . . . . 9  |-  ( ph  ->  P  e.  ( ZZ>= `  ( Q  +  2
) ) )
130 efgredlemd.sc . . . . . . . . 9  |-  ( ph  ->  ( S `  C
)  =  ( ( ( B `  L
) substr  <. 0 ,  Q >. ) concat  ( ( A `
 K ) substr  <. ( Q  +  2 ) ,  ( # `  ( A `  K )
) >. ) ) )
1312, 3, 4, 5, 6, 7, 29, 13, 30, 31, 32, 28, 64, 122, 123, 124, 125, 126, 127, 128, 129, 1, 130efgredleme 15068 . . . . . . . 8  |-  ( ph  ->  ( ( A `  K )  e.  ran  ( T `  ( S `
 C ) )  /\  ( B `  L )  e.  ran  ( T `  ( S `
 C ) ) ) )
132131simpld 445 . . . . . . 7  |-  ( ph  ->  ( A `  K
)  e.  ran  ( T `  ( S `  C ) ) )
1332, 3, 4, 5, 6, 7efgsp1 15062 . . . . . . 7  |-  ( ( C  e.  dom  S  /\  ( A `  K
)  e.  ran  ( T `  ( S `  C ) ) )  ->  ( C concat  <" ( A `  K ) "> )  e.  dom  S )
1341, 132, 133syl2anc 642 . . . . . 6  |-  ( ph  ->  ( C concat  <" ( A `  K ) "> )  e.  dom  S )
1352, 3, 4, 5, 6, 7efgsval2 15058 . . . . . 6  |-  ( ( C  e. Word  W  /\  ( A `  K )  e.  W  /\  ( C concat  <" ( A `
 K ) "> )  e.  dom  S )  ->  ( S `  ( C concat  <" ( A `  K ) "> ) )  =  ( A `  K
) )
13612, 40, 134, 135syl3anc 1182 . . . . 5  |-  ( ph  ->  ( S `  ( C concat  <" ( A `
 K ) "> ) )  =  ( A `  K
) )
137111, 136eqtr4d 2331 . . . 4  |-  ( ph  ->  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `
 K ) "> ) ) )
138 fveq2 5541 . . . . . . . . 9  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( S `  a
)  =  ( S `
 ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ) )
139138fveq2d 5545 . . . . . . . 8  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( # `  ( S `
 a ) )  =  ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) ) )
140139breq1d 4049 . . . . . . 7  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  <->  ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) ) ) )
141138eqeq1d 2304 . . . . . . . 8  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( ( S `  a )  =  ( S `  b )  <-> 
( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  b
) ) )
142 fveq1 5540 . . . . . . . . 9  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( a `  0
)  =  ( ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) `  0
) )
143142eqeq1d 2304 . . . . . . . 8  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( ( a ` 
0 )  =  ( b `  0 )  <-> 
( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( b `  0 ) ) )
144141, 143imbi12d 311 . . . . . . 7  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( ( ( S `
 a )  =  ( S `  b
)  ->  ( a `  0 )  =  ( b `  0
) )  <->  ( ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) )  =  ( S `  b )  ->  ( ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) `  0 )  =  ( b ` 
0 ) ) ) )
145140, 144imbi12d 311 . . . . . 6  |-  ( a  =  ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  -> 
( ( ( # `  ( S `  a
) )  <  ( # `
 ( S `  A ) )  -> 
( ( S `  a )  =  ( S `  b )  ->  ( a ` 
0 )  =  ( b `  0 ) ) )  <->  ( ( # `
 ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) )  =  ( S `  b )  ->  ( ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) `  0 )  =  ( b ` 
0 ) ) ) ) )
146 fveq2 5541 . . . . . . . . 9  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  ( S `  b )  =  ( S `  ( C concat  <" ( A `  K ) "> ) ) )
147146eqeq2d 2307 . . . . . . . 8  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  (
( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  b
)  <->  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `
 K ) "> ) ) ) )
148 fveq1 5540 . . . . . . . . 9  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  (
b `  0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0 )
)
149148eqeq2d 2307 . . . . . . . 8  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  (
( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( b `  0 )  <-> 
( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) ) )
150147, 149imbi12d 311 . . . . . . 7  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  (
( ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  b
)  ->  ( ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) `  0
)  =  ( b `
 0 ) )  <-> 
( ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `
 K ) "> ) )  -> 
( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) ) ) )
151150imbi2d 307 . . . . . 6  |-  ( b  =  ( C concat  <" ( A `  K ) "> )  ->  (
( ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) )  =  ( S `  b )  ->  (
( A  |`  (
0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( b `  0 ) ) )  <->  ( ( # `
 ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `  K ) "> ) )  ->  (
( A  |`  (
0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) ) ) ) )
152145, 151rspc2va 2904 . . . . 5  |-  ( ( ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) )  e. 
dom  S  /\  ( C concat  <" ( A `
 K ) "> )  e.  dom  S )  /\  A. a  e.  dom  S A. b  e.  dom  S ( (
# `  ( S `  a ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 a )  =  ( S `  b
)  ->  ( a `  0 )  =  ( b `  0
) ) ) )  ->  ( ( # `  ( S `  ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `  K ) "> ) )  ->  (
( A  |`  (
0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) ) ) )
15391, 134, 29, 152syl21anc 1181 . . . 4  |-  ( ph  ->  ( ( # `  ( S `  ( A  |`  ( 0..^ ( (
# `  A )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( A `  K ) "> ) )  -> 
( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) ) ) )
154121, 137, 153mp2d 41 . . 3  |-  ( ph  ->  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( A `  K ) "> ) `  0
) )
15577, 71sseldi 3191 . . . . . . . 8  |-  ( ph  ->  ( B `  L
)  e. Word  ( I  X.  2o ) )
156 lencl 11437 . . . . . . . 8  |-  ( ( B `  L )  e. Word  ( I  X.  2o )  ->  ( # `  ( B `  L
) )  e.  NN0 )
157155, 156syl 15 . . . . . . 7  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  NN0 )
158157nn0red 10035 . . . . . 6  |-  ( ph  ->  ( # `  ( B `  L )
)  e.  RR )
159 ltaddrp 10402 . . . . . 6  |-  ( ( ( # `  ( B `  L )
)  e.  RR  /\  2  e.  RR+ )  -> 
( # `  ( B `
 L ) )  <  ( ( # `  ( B `  L
) )  +  2 ) )
160158, 82, 159sylancl 643 . . . . 5  |-  ( ph  ->  ( # `  ( B `  L )
)  <  ( ( # `
 ( B `  L ) )  +  2 ) )
16159nn0red 10035 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  B
)  e.  RR )
162161lem1d 9706 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  B
)  -  1 )  <_  ( # `  B
) )
163 fznn 10868 . . . . . . . . . . 11  |-  ( (
# `  B )  e.  ZZ  ->  ( (
( # `  B )  -  1 )  e.  ( 1 ... ( # `
 B ) )  <-> 
( ( ( # `  B )  -  1 )  e.  NN  /\  ( ( # `  B
)  -  1 )  <_  ( # `  B
) ) ) )
16460, 163syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( # `  B )  -  1 )  e.  ( 1 ... ( # `  B
) )  <->  ( (
( # `  B )  -  1 )  e.  NN  /\  ( (
# `  B )  -  1 )  <_ 
( # `  B ) ) ) )
16565, 162, 164mpbir2and 888 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  B
)  -  1 )  e.  ( 1 ... ( # `  B
) ) )
1662, 3, 4, 5, 6, 7efgsres 15063 . . . . . . . . 9  |-  ( ( B  e.  dom  S  /\  ( ( # `  B
)  -  1 )  e.  ( 1 ... ( # `  B
) ) )  -> 
( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) )  e. 
dom  S )
16730, 165, 166syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) )  e. 
dom  S )
1682, 3, 4, 5, 6, 7efgsval 15056 . . . . . . . 8  |-  ( ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) )  e.  dom  S  ->  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) `  ( ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  - 
1 ) ) )
169167, 168syl 15 . . . . . . 7  |-  ( ph  ->  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) `  ( ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  - 
1 ) ) )
170 fzss1 10846 . . . . . . . . . . . . . . 15  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... ( # `  B
) )  C_  (
0 ... ( # `  B
) ) )
17196, 170ax-mp 8 . . . . . . . . . . . . . 14  |-  ( 1 ... ( # `  B
) )  C_  (
0 ... ( # `  B
) )
172171, 165sseldi 3191 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( # `  B
)  -  1 )  e.  ( 0 ... ( # `  B
) ) )
173 swrd0val 11470 . . . . . . . . . . . . 13  |-  ( ( B  e. Word  W  /\  ( ( # `  B
)  -  1 )  e.  ( 0 ... ( # `  B
) ) )  -> 
( B substr  <. 0 ,  ( ( # `  B
)  -  1 )
>. )  =  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )
17454, 172, 173syl2anc 642 . . . . . . . . . . . 12  |-  ( ph  ->  ( B substr  <. 0 ,  ( ( # `  B )  -  1 ) >. )  =  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )
175174fveq2d 5545 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( B substr  <. 0 ,  ( ( # `  B
)  -  1 )
>. ) )  =  (
# `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )
176 swrd0len 11471 . . . . . . . . . . . 12  |-  ( ( B  e. Word  W  /\  ( ( # `  B
)  -  1 )  e.  ( 0 ... ( # `  B
) ) )  -> 
( # `  ( B substr  <. 0 ,  ( (
# `  B )  -  1 ) >.
) )  =  ( ( # `  B
)  -  1 ) )
17754, 172, 176syl2anc 642 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  ( B substr  <. 0 ,  ( ( # `  B
)  -  1 )
>. ) )  =  ( ( # `  B
)  -  1 ) )
178175, 177eqtr3d 2330 . . . . . . . . . 10  |-  ( ph  ->  ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( ( # `  B
)  -  1 ) )
179178oveq1d 5889 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  - 
1 )  =  ( ( ( # `  B
)  -  1 )  -  1 ) )
180179, 64syl6eqr 2346 . . . . . . . 8  |-  ( ph  ->  ( ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  - 
1 )  =  L )
181180fveq2d 5545 . . . . . . 7  |-  ( ph  ->  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) `  ( ( # `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  - 
1 ) )  =  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) `  L ) )
182 fvres 5558 . . . . . . . 8  |-  ( L  e.  ( 0..^ ( ( # `  B
)  -  1 ) )  ->  ( ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) `  L
)  =  ( B `
 L ) )
18368, 182syl 15 . . . . . . 7  |-  ( ph  ->  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) `  L )  =  ( B `  L ) )
184169, 181, 1833eqtrd 2332 . . . . . 6  |-  ( ph  ->  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( B `  L
) )
185184fveq2d 5545 . . . . 5  |-  ( ph  ->  ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )  =  ( # `  ( B `  L )
) )
1862, 3, 4, 5, 6, 7efgsdmi 15057 . . . . . . . . 9  |-  ( ( B  e.  dom  S  /\  ( ( # `  B
)  -  1 )  e.  NN )  -> 
( S `  B
)  e.  ran  ( T `  ( B `  ( ( ( # `  B )  -  1 )  -  1 ) ) ) )
18730, 65, 186syl2anc 642 . . . . . . . 8  |-  ( ph  ->  ( S `  B
)  e.  ran  ( T `  ( B `  ( ( ( # `  B )  -  1 )  -  1 ) ) ) )
18831, 187eqeltrd 2370 . . . . . . 7  |-  ( ph  ->  ( S `  A
)  e.  ran  ( T `  ( B `  ( ( ( # `  B )  -  1 )  -  1 ) ) ) )
18964fveq2i 5544 . . . . . . . . 9  |-  ( B `
 L )  =  ( B `  (
( ( # `  B
)  -  1 )  -  1 ) )
190189fveq2i 5544 . . . . . . . 8  |-  ( T `
 ( B `  L ) )  =  ( T `  ( B `  ( (
( # `  B )  -  1 )  - 
1 ) ) )
191190rneqi 4921 . . . . . . 7  |-  ran  ( T `  ( B `  L ) )  =  ran  ( T `  ( B `  ( ( ( # `  B
)  -  1 )  -  1 ) ) )
192188, 191syl6eleqr 2387 . . . . . 6  |-  ( ph  ->  ( S `  A
)  e.  ran  ( T `  ( B `  L ) ) )
1932, 3, 4, 5efgtlen 15051 . . . . . 6  |-  ( ( ( B `  L
)  e.  W  /\  ( S `  A )  e.  ran  ( T `
 ( B `  L ) ) )  ->  ( # `  ( S `  A )
)  =  ( (
# `  ( B `  L ) )  +  2 ) )
19471, 192, 193syl2anc 642 . . . . 5  |-  ( ph  ->  ( # `  ( S `  A )
)  =  ( (
# `  ( B `  L ) )  +  2 ) )
195160, 185, 1943brtr4d 4069 . . . 4  |-  ( ph  ->  ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) ) )
196131simprd 449 . . . . . . 7  |-  ( ph  ->  ( B `  L
)  e.  ran  ( T `  ( S `  C ) ) )
1972, 3, 4, 5, 6, 7efgsp1 15062 . . . . . . 7  |-  ( ( C  e.  dom  S  /\  ( B `  L
)  e.  ran  ( T `  ( S `  C ) ) )  ->  ( C concat  <" ( B `  L ) "> )  e.  dom  S )
1981, 196, 197syl2anc 642 . . . . . 6  |-  ( ph  ->  ( C concat  <" ( B `  L ) "> )  e.  dom  S )
1992, 3, 4, 5, 6, 7efgsval2 15058 . . . . . 6  |-  ( ( C  e. Word  W  /\  ( B `  L )  e.  W  /\  ( C concat  <" ( B `
 L ) "> )  e.  dom  S )  ->  ( S `  ( C concat  <" ( B `  L ) "> ) )  =  ( B `  L
) )
20012, 71, 198, 199syl3anc 1182 . . . . 5  |-  ( ph  ->  ( S `  ( C concat  <" ( B `
 L ) "> ) )  =  ( B `  L
) )
201184, 200eqtr4d 2331 . . . 4  |-  ( ph  ->  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `
 L ) "> ) ) )
202 fveq2 5541 . . . . . . . . 9  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( S `  a
)  =  ( S `
 ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ) )
203202fveq2d 5545 . . . . . . . 8  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( # `  ( S `
 a ) )  =  ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) ) )
204203breq1d 4049 . . . . . . 7  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( ( # `  ( S `  a )
)  <  ( # `  ( S `  A )
)  <->  ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) ) ) )
205202eqeq1d 2304 . . . . . . . 8  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( ( S `  a )  =  ( S `  b )  <-> 
( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  b
) ) )
206 fveq1 5540 . . . . . . . . 9  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( a `  0
)  =  ( ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) `  0
) )
207206eqeq1d 2304 . . . . . . . 8  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( ( a ` 
0 )  =  ( b `  0 )  <-> 
( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( b `  0 ) ) )
208205, 207imbi12d 311 . . . . . . 7  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( ( ( S `
 a )  =  ( S `  b
)  ->  ( a `  0 )  =  ( b `  0
) )  <->  ( ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) )  =  ( S `  b )  ->  ( ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) `  0 )  =  ( b ` 
0 ) ) ) )
209204, 208imbi12d 311 . . . . . 6  |-  ( a  =  ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  -> 
( ( ( # `  ( S `  a
) )  <  ( # `
 ( S `  A ) )  -> 
( ( S `  a )  =  ( S `  b )  ->  ( a ` 
0 )  =  ( b `  0 ) ) )  <->  ( ( # `
 ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) )  =  ( S `  b )  ->  ( ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) `  0 )  =  ( b ` 
0 ) ) ) ) )
210 fveq2 5541 . . . . . . . . 9  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  ( S `  b )  =  ( S `  ( C concat  <" ( B `  L ) "> ) ) )
211210eqeq2d 2307 . . . . . . . 8  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  (
( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  b
)  <->  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `
 L ) "> ) ) ) )
212 fveq1 5540 . . . . . . . . 9  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  (
b `  0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0 )
)
213212eqeq2d 2307 . . . . . . . 8  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  (
( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( b `  0 )  <-> 
( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) ) )
214211, 213imbi12d 311 . . . . . . 7  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  (
( ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  b
)  ->  ( ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) `  0
)  =  ( b `
 0 ) )  <-> 
( ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `
 L ) "> ) )  -> 
( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) ) ) )
215214imbi2d 307 . . . . . 6  |-  ( b  =  ( C concat  <" ( B `  L ) "> )  ->  (
( ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) )  =  ( S `  b )  ->  (
( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( b `  0 ) ) )  <->  ( ( # `
 ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `  L ) "> ) )  ->  (
( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) ) ) ) )
216209, 215rspc2va 2904 . . . . 5  |-  ( ( ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) )  e. 
dom  S  /\  ( C concat  <" ( B `
 L ) "> )  e.  dom  S )  /\  A. a  e.  dom  S A. b  e.  dom  S ( (
# `  ( S `  a ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 a )  =  ( S `  b
)  ->  ( a `  0 )  =  ( b `  0
) ) ) )  ->  ( ( # `  ( S `  ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) ) )  <  ( # `  ( S `  A )
)  ->  ( ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `  L ) "> ) )  ->  (
( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) ) ) )
217167, 198, 29, 216syl21anc 1181 . . . 4  |-  ( ph  ->  ( ( # `  ( S `  ( B  |`  ( 0..^ ( (
# `  B )  -  1 ) ) ) ) )  < 
( # `  ( S `
 A ) )  ->  ( ( S `
 ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) )  =  ( S `  ( C concat  <" ( B `  L ) "> ) )  -> 
( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) ) ) )
218195, 201, 217mp2d 41 . . 3  |-  ( ph  ->  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( ( C concat  <" ( B `  L ) "> ) `  0
) )
21975, 154, 2183eqtr4d 2338 . 2  |-  ( ph  ->  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( ( B  |`  (
0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 ) )
220 lbfzo0 10919 . . . 4  |-  ( 0  e.  ( 0..^ ( ( # `  A
)  -  1 ) )  <->  ( ( # `  A )  -  1 )  e.  NN )
22134, 220sylibr 203 . . 3  |-  ( ph  ->  0  e.  ( 0..^ ( ( # `  A
)  -  1 ) ) )
222 fvres 5558 . . 3  |-  ( 0  e.  ( 0..^ ( ( # `  A
)  -  1 ) )  ->  ( ( A  |`  ( 0..^ ( ( # `  A
)  -  1 ) ) ) `  0
)  =  ( A `
 0 ) )
223221, 222syl 15 . 2  |-  ( ph  ->  ( ( A  |`  ( 0..^ ( ( # `  A )  -  1 ) ) ) ` 
0 )  =  ( A `  0 ) )
224 lbfzo0 10919 . . . 4  |-  ( 0  e.  ( 0..^ ( ( # `  B
)  -  1 ) )  <->  ( ( # `  B )  -  1 )  e.  NN )
22565, 224sylibr 203 . . 3  |-  ( ph  ->  0  e.  ( 0..^ ( ( # `  B
)  -  1 ) ) )
226 fvres 5558 . . 3  |-  ( 0  e.  ( 0..^ ( ( # `  B
)  -  1 ) )  ->  ( ( B  |`  ( 0..^ ( ( # `  B
)  -  1 ) ) ) `  0
)  =  ( B `
 0 ) )
227225, 226syl 15 . 2  |-  ( ph  ->  ( ( B  |`  ( 0..^ ( ( # `  B )  -  1 ) ) ) ` 
0 )  =  ( B `  0 ) )
228219, 223, 2273eqtr3d 2336 1  |-  ( ph  ->  ( A `  0
)  =  ( B `
 0 ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   {crab 2560    \ cdif 3162    C_ wss 3165   (/)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    |` cres 4707   -->wf 5267   ` cfv 5271  (class class class)co 5874    e. cmpt2 5876   1oc1o 6488   2oc2o 6489   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    < clt 8883    <_ cle 8884    - cmin 9053   NNcn 9762   2c2 9811   NN0cn0 9981   ZZcz 10040   ZZ>=cuz 10246   RR+crp 10370   ...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:  efgredlemc  15070
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