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

Theorem wrd2ind 12759
Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019.)
Hypotheses
Ref Expression
wrd2ind.1  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ( ph 
<->  ps ) )
wrd2ind.2  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ph  <->  ch )
)
wrd2ind.3  |-  ( ( x  =  ( y ++ 
<" z "> )  /\  w  =  ( u ++  <" s "> ) )  -> 
( ph  <->  th ) )
wrd2ind.4  |-  ( x  =  A  ->  ( rh 
<->  ta ) )
wrd2ind.5  |-  ( w  =  B  ->  ( ph 
<->  rh ) )
wrd2ind.6  |-  ps
wrd2ind.7  |-  ( ( ( y  e. Word  X  /\  z  e.  X
)  /\  ( u  e. Word  Y  /\  s  e.  Y )  /\  ( # `
 y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
Assertion
Ref Expression
wrd2ind  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ta )
Distinct variable groups:    x, w, A    y, w, z, B, x    u, s, w, x, y, z, X    Y, s, u, w, x, y, z    ch, w, x    ph, s, u, y, z    ta, x    th, w, x    rh, w
Allowed substitution hints:    ph( x, w)    ps( x, y, z, w, u, s)    ch( y,
z, u, s)    th( y,
z, u, s)    ta( y, z, w, u, s)    rh( x, y, z, u, s)    A( y, z, u, s)    B( u, s)

Proof of Theorem wrd2ind
Dummy variables  n  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lencl 12614 . . . . 5  |-  ( A  e. Word  X  ->  ( # `
 A )  e. 
NN0 )
2 eqeq2 2417 . . . . . . . . 9  |-  ( n  =  0  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  0 ) )
32anbi2d 702 . . . . . . . 8  |-  ( n  =  0  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 ) ) )
43imbi1d 315 . . . . . . 7  |-  ( n  =  0  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 )  ->  ph ) ) )
542ralbidv 2848 . . . . . 6  |-  ( n  =  0  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  0 )  ->  ph )
) )
6 eqeq2 2417 . . . . . . . . 9  |-  ( n  =  m  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  m ) )
76anbi2d 702 . . . . . . . 8  |-  ( n  =  m  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  m ) ) )
87imbi1d 315 . . . . . . 7  |-  ( n  =  m  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph ) ) )
982ralbidv 2848 . . . . . 6  |-  ( n  =  m  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  m )  ->  ph )
) )
10 eqeq2 2417 . . . . . . . . 9  |-  ( n  =  ( m  + 
1 )  ->  (
( # `  x )  =  n  <->  ( # `  x
)  =  ( m  +  1 ) ) )
1110anbi2d 702 . . . . . . . 8  |-  ( n  =  ( m  + 
1 )  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  <->  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )
1211imbi1d 315 . . . . . . 7  |-  ( n  =  ( m  + 
1 )  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  n )  ->  ph )  <->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) ) )
13122ralbidv 2848 . . . . . 6  |-  ( n  =  ( m  + 
1 )  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ph )
) )
14 eqeq2 2417 . . . . . . . . 9  |-  ( n  =  ( # `  A
)  ->  ( ( # `
 x )  =  n  <->  ( # `  x
)  =  ( # `  A ) ) )
1514anbi2d 702 . . . . . . . 8  |-  ( n  =  ( # `  A
)  ->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  n )  <-> 
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) ) ) )
1615imbi1d 315 . . . . . . 7  |-  ( n  =  ( # `  A
)  ->  ( (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  n )  ->  ph )  <->  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )
) )
17162ralbidv 2848 . . . . . 6  |-  ( n  =  ( # `  A
)  ->  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  n )  ->  ph )  <->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) ) )
18 eqeq1 2406 . . . . . . . . . . . 12  |-  ( (
# `  x )  =  0  ->  (
( # `  x )  =  ( # `  w
)  <->  0  =  (
# `  w )
) )
1918adantl 464 . . . . . . . . . . 11  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( ( # `  x )  =  (
# `  w )  <->  0  =  ( # `  w
) ) )
20 eqcom 2411 . . . . . . . . . . . . . . 15  |-  ( 0  =  ( # `  w
)  <->  ( # `  w
)  =  0 )
21 hasheq0 12481 . . . . . . . . . . . . . . 15  |-  ( w  e. Word  Y  ->  (
( # `  w )  =  0  <->  w  =  (/) ) )
2220, 21syl5bb 257 . . . . . . . . . . . . . 14  |-  ( w  e. Word  Y  ->  (
0  =  ( # `  w )  <->  w  =  (/) ) )
23 hasheq0 12481 . . . . . . . . . . . . . . . 16  |-  ( x  e. Word  X  ->  (
( # `  x )  =  0  <->  x  =  (/) ) )
24 wrd2ind.6 . . . . . . . . . . . . . . . . . 18  |-  ps
25 wrd2ind.1 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ( ph 
<->  ps ) )
2624, 25mpbiri 233 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  (/)  /\  w  =  (/) )  ->  ph )
2726ex 432 . . . . . . . . . . . . . . . 16  |-  ( x  =  (/)  ->  ( w  =  (/)  ->  ph )
)
2823, 27syl6bi 228 . . . . . . . . . . . . . . 15  |-  ( x  e. Word  X  ->  (
( # `  x )  =  0  ->  (
w  =  (/)  ->  ph )
) )
2928com13 80 . . . . . . . . . . . . . 14  |-  ( w  =  (/)  ->  ( (
# `  x )  =  0  ->  (
x  e. Word  X  ->  ph ) ) )
3022, 29syl6bi 228 . . . . . . . . . . . . 13  |-  ( w  e. Word  Y  ->  (
0  =  ( # `  w )  ->  (
( # `  x )  =  0  ->  (
x  e. Word  X  ->  ph ) ) ) )
3130com24 87 . . . . . . . . . . . 12  |-  ( w  e. Word  Y  ->  (
x  e. Word  X  ->  ( ( # `  x
)  =  0  -> 
( 0  =  (
# `  w )  ->  ph ) ) ) )
3231imp31 430 . . . . . . . . . . 11  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( 0  =  ( # `  w
)  ->  ph ) )
3319, 32sylbid 215 . . . . . . . . . 10  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( # `  x
)  =  0 )  ->  ( ( # `  x )  =  (
# `  w )  ->  ph ) )
3433ex 432 . . . . . . . . 9  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( # `  x
)  =  0  -> 
( ( # `  x
)  =  ( # `  w )  ->  ph )
) )
3534com23 78 . . . . . . . 8  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( # `  x
)  =  ( # `  w )  ->  (
( # `  x )  =  0  ->  ph )
) )
3635impd 429 . . . . . . 7  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  0 )  ->  ph ) )
3736rgen2 2829 . . . . . 6  |-  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  0 )  ->  ph )
38 fveq2 5849 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  ( # `
 x )  =  ( # `  y
) )
39 fveq2 5849 . . . . . . . . . . . . 13  |-  ( w  =  u  ->  ( # `
 w )  =  ( # `  u
) )
4038, 39eqeqan12d 2425 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( # `  x
)  =  ( # `  w )  <->  ( # `  y
)  =  ( # `  u ) ) )
4138eqeq1d 2404 . . . . . . . . . . . . 13  |-  ( x  =  y  ->  (
( # `  x )  =  m  <->  ( # `  y
)  =  m ) )
4241adantr 463 . . . . . . . . . . . 12  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( # `  x
)  =  m  <->  ( # `  y
)  =  m ) )
4340, 42anbi12d 709 . . . . . . . . . . 11  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  m )  <-> 
( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m ) ) )
44 wrd2ind.2 . . . . . . . . . . 11  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ph  <->  ch )
)
4543, 44imbi12d 318 . . . . . . . . . 10  |-  ( ( x  =  y  /\  w  =  u )  ->  ( ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  ( (
( # `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) ) )
4645ancoms 451 . . . . . . . . 9  |-  ( ( w  =  u  /\  x  =  y )  ->  ( ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  ( (
( # `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) ) )
4746cbvraldva 3040 . . . . . . . 8  |-  ( w  =  u  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  m )  ->  ph )  <->  A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) ) )
4847cbvralv 3034 . . . . . . 7  |-  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  <->  A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) )
49 swrdcl 12700 . . . . . . . . . . . . . . . . 17  |-  ( w  e. Word  Y  ->  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y )
5049adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y
)
5150ad2antrl 726 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y )
52 simprll 764 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  e. Word  Y )
53 eqeq1 2406 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  =  ( # `  w
)  <->  ( m  + 
1 )  =  (
# `  w )
) )
54 nn0p1nn 10876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( m  e.  NN0  ->  ( m  +  1 )  e.  NN )
55 eleq1 2474 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
# `  w )  =  ( m  + 
1 )  ->  (
( # `  w )  e.  NN  <->  ( m  +  1 )  e.  NN ) )
5655eqcoms 2414 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( m  +  1 )  =  ( # `  w
)  ->  ( ( # `
 w )  e.  NN  <->  ( m  + 
1 )  e.  NN ) )
5754, 56syl5ibr 221 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( m  +  1 )  =  ( # `  w
)  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) )
5853, 57syl6bi 228 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  =  ( # `  w
)  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) ) )
5958impcom 428 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  (
m  e.  NN0  ->  (
# `  w )  e.  NN ) )
6059adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) )  ->  ( m  e.  NN0  ->  ( # `  w
)  e.  NN ) )
6160impcom 428 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  e.  NN )
6261nnge1d 10619 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  1  <_  ( # `  w
) )
63 wrdlenge1n0 12629 . . . . . . . . . . . . . . . . . 18  |-  ( w  e. Word  Y  ->  (
w  =/=  (/)  <->  1  <_  (
# `  w )
) )
6452, 63syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w  =/=  (/)  <->  1  <_  (
# `  w )
) )
6562, 64mpbird 232 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  =/=  (/) )
66 lswcl 12642 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  w  =/=  (/) )  ->  ( lastS  `  w )  e.  Y
)
6752, 65, 66syl2anc 659 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( lastS  `  w )  e.  Y
)
6851, 67jca 530 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  e. Word  Y  /\  ( lastS  `  w )  e.  Y ) )
69 swrdcl 12700 . . . . . . . . . . . . . . . 16  |-  ( x  e. Word  X  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
7069adantl 464 . . . . . . . . . . . . . . 15  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X
)
7170ad2antrl 726 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
72 simprlr 765 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  e. Word  X )
73 eleq1 2474 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
( # `  x )  e.  NN  <->  ( m  +  1 )  e.  NN ) )
7454, 73syl5ibr 221 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  x )  =  ( m  + 
1 )  ->  (
m  e.  NN0  ->  (
# `  x )  e.  NN ) )
7574ad2antll 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) )  ->  ( m  e.  NN0  ->  ( # `  x
)  e.  NN ) )
7675impcom 428 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  e.  NN )
7776nnge1d 10619 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  1  <_  ( # `  x
) )
78 wrdlenge1n0 12629 . . . . . . . . . . . . . . . . 17  |-  ( x  e. Word  X  ->  (
x  =/=  (/)  <->  1  <_  (
# `  x )
) )
7972, 78syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
x  =/=  (/)  <->  1  <_  (
# `  x )
) )
8077, 79mpbird 232 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  =/=  (/) )
81 lswcl 12642 . . . . . . . . . . . . . . 15  |-  ( ( x  e. Word  X  /\  x  =/=  (/) )  ->  ( lastS  `  x )  e.  X
)
8272, 80, 81syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( lastS  `  x )  e.  X
)
8368, 71, 82jca32 533 . . . . . . . . . . . . 13  |-  ( ( m  e.  NN0  /\  ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  ( ( # `
 x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( lastS  `  w )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( lastS  `  x )  e.  X ) ) )
8483adantlr 713 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( lastS  `  w )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( lastS  `  x )  e.  X ) ) )
85 simprl 756 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
w  e. Word  Y  /\  x  e. Word  X )
)
86 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch ) )
87 simprrl 766 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  =  ( # `  w
) )
8887oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  =  ( ( # `  w
)  -  1 ) )
89 simprlr 765 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  e. Word  X )
90 fzossfz 11877 . . . . . . . . . . . . . . . . . 18  |-  ( 0..^ ( # `  x
) )  C_  (
0 ... ( # `  x
) )
91 simprrr 767 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  =  ( m  +  1 ) )
9254ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
m  +  1 )  e.  NN )
9391, 92eqeltrd 2490 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 x )  e.  NN )
94 fzo0end 11941 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  x )  e.  NN  ->  ( ( # `
 x )  - 
1 )  e.  ( 0..^ ( # `  x
) ) )
9593, 94syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  e.  ( 0..^ ( # `  x ) ) )
9690, 95sseldi 3440 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  e.  ( 0 ... ( # `
 x ) ) )
97 swrd0len 12703 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e. Word  X  /\  ( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) )  -> 
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  ( ( # `  x
)  -  1 ) )
9889, 96, 97syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( ( # `  x
)  -  1 ) )
99 simprll 764 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  e. Word  Y )
100 oveq1 6285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( ( # `
 w )  - 
1 )  =  ( ( # `  x
)  -  1 ) )
101 oveq2 6286 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( 0 ... ( # `  w
) )  =  ( 0 ... ( # `  x ) ) )
102100, 101eleq12d 2484 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
# `  w )  =  ( # `  x
)  ->  ( (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) )  <-> 
( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) ) )
103102eqcoms 2414 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
# `  x )  =  ( # `  w
)  ->  ( (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) )  <-> 
( ( # `  x
)  -  1 )  e.  ( 0 ... ( # `  x
) ) ) )
104103adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  (
( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) )  <->  ( ( # `
 x )  - 
1 )  e.  ( 0 ... ( # `  x ) ) ) )
105104ad2antll 727 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) )  <->  ( ( # `
 x )  - 
1 )  e.  ( 0 ... ( # `  x ) ) ) )
10696, 105mpbird 232 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  w )  -  1 )  e.  ( 0 ... ( # `
 w ) ) )
107 swrd0len 12703 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e. Word  Y  /\  ( ( # `  w
)  -  1 )  e.  ( 0 ... ( # `  w
) ) )  -> 
( # `  ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) )  =  ( ( # `  w
)  -  1 ) )
10899, 106, 107syl2anc 659 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) )  =  ( ( # `  w
)  -  1 ) )
10988, 98, 1083eqtr4d 2453 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )
11091oveq1d 6293 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  -  1 )  =  ( ( m  + 
1 )  -  1 ) )
111 nn0cn 10846 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN0  ->  m  e.  CC )
112111ad2antrr 724 . . . . . . . . . . . . . . . . 17  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  m  e.  CC )
113 ax-1cn 9580 . . . . . . . . . . . . . . . . 17  |-  1  e.  CC
114 pncan 9862 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  CC  /\  1  e.  CC )  ->  ( ( m  + 
1 )  -  1 )  =  m )
115112, 113, 114sylancl 660 . . . . . . . . . . . . . . . 16  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( m  +  1 )  -  1 )  =  m )
11698, 110, 1153eqtrd 2447 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )
117109, 116jca 530 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m ) )
11870adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  e. Word  X )
119 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( # `
 y )  =  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ) )
120 fveq2 5849 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( # `
 u )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )
121119, 120eqeqan12d 2425 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
( # `  y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
122121expcom 433 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  ->  ( ( # `
 y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
123122adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  (
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  ->  ( ( # `
 y )  =  ( # `  u
)  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
124123imp 427 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( # `  y
)  =  ( # `  u )  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
125119eqeq1d 2404 . . . . . . . . . . . . . . . . . . 19  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( # `  y )  =  m  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  m ) )
126125adantl 464 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( # `  y
)  =  m  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  m ) )
127124, 126anbi12d 709 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( ( # `  y )  =  (
# `  u )  /\  ( # `  y
)  =  m )  <-> 
( ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m ) ) )
128 vex 3062 . . . . . . . . . . . . . . . . . . . . 21  |-  y  e. 
_V
129 vex 3062 . . . . . . . . . . . . . . . . . . . . 21  |-  u  e. 
_V
130128, 129, 44sbc2ie 3345 . . . . . . . . . . . . . . . . . . . 20  |-  ( [. y  /  x ]. [. u  /  w ]. ph  <->  ch )
131130bicomi 202 . . . . . . . . . . . . . . . . . . 19  |-  ( ch  <->  [. y  /  x ]. [. u  /  w ]. ph )
132131a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ch  <->  [. y  /  x ]. [. u  /  w ]. ph ) )
133 simpr 459 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
y  =  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )
134133sbceq1d 3282 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( [. y  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph ) )
135 dfsbcq 3279 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. ph  <->  [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
136135sbcbidv 3332 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
137136adantl 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
138137adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. u  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
139132, 134, 1383bitrd 279 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ch  <->  [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
140127, 139imbi12d 318 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( w  e. Word  Y  /\  x  e. Word  X
)  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  -> 
( ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch )  <->  ( (
( # `  ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
141118, 140rspcdv 3163 . . . . . . . . . . . . . . 15  |-  ( ( ( w  e. Word  Y  /\  x  e. Word  X )  /\  u  =  ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  ->  ( A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch )  ->  ( ( (
# `  ( x substr  <.
0 ,  ( (
# `  x )  -  1 ) >.
) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
14250, 141rspcimdv 3161 . . . . . . . . . . . . . 14  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  ( A. u  e. Word  Y A. y  e. Word  X
( ( ( # `  y )  =  (
# `  u )  /\  ( # `  y
)  =  m )  ->  ch )  -> 
( ( ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  /\  ( # `
 ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  m )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) ) )
14385, 86, 117, 142syl3c 60 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  [. (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph )
144143, 109jca 530 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) ) )
145 dfsbcq 3279 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  <->  [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. [. y  /  x ]. ph ) )
146 sbccom 3349 . . . . . . . . . . . . . . . 16  |-  ( [. ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. [. y  /  x ]. ph  <->  [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph )
147145, 146syl6bb 261 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  <->  [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
148120eqeq2d 2416 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( # `  y )  =  ( # `  u
)  <->  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) ) )
149147, 148anbi12d 709 . . . . . . . . . . . . . 14  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  (
# `  u )
)  <->  ( [. y  /  x ]. [. (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) ) )
150 oveq1 6285 . . . . . . . . . . . . . . 15  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
u ++  <" s "> )  =  ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" s "> ) )
151150sbceq1d 3282 . . . . . . . . . . . . . 14  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  ( [. ( u ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )
)
152149, 151imbi12d 318 . . . . . . . . . . . . 13  |-  ( u  =  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  ->  (
( ( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  ( # `  u
) )  ->  [. (
u ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )
) )
153 s1eq 12666 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( lastS  `  w
)  ->  <" s ">  =  <" ( lastS  `  w ) "> )
154153oveq2d 6294 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( lastS  `  w
)  ->  ( (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" s "> )  =  ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" ( lastS  `  w ) "> ) )
155154sbceq1d 3282 . . . . . . . . . . . . . . 15  |-  ( s  =  ( lastS  `  w
)  ->  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph ) )
156155imbi2d 314 . . . . . . . . . . . . . 14  |-  ( s  =  ( lastS  `  w
)  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph ) ) )
157 sbccom 3349 . . . . . . . . . . . . . . . 16  |-  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" ( lastS  `  w ) "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph  <->  [. ( y ++  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
158157a1i 11 . . . . . . . . . . . . . . 15  |-  ( s  =  ( lastS  `  w
)  ->  ( [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" ( lastS  `  w ) "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph  <->  [. ( y ++  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
159158imbi2d 314 . . . . . . . . . . . . . 14  |-  ( s  =  ( lastS  `  w
)  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" ( lastS  `  w ) "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( y ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph )
) )
160156, 159bitrd 253 . . . . . . . . . . . . 13  |-  ( s  =  ( lastS  `  w
)  ->  ( (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )  <->  ( ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
)  /  w ]. ph 
/\  ( # `  y
)  =  ( # `  ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. ) ) )  ->  [. ( y ++  <" z "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
) )
161 dfsbcq 3279 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  <->  [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph ) )
162119eqeq1d 2404 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( # `  y )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) )  <->  ( # `  (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) ) )
163161, 162anbi12d 709 . . . . . . . . . . . . . 14  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( [. y  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  <->  ( [. ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) ) ) )
164 oveq1 6285 . . . . . . . . . . . . . . 15  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
y ++  <" z "> )  =  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" z "> ) )
165164sbceq1d 3282 . . . . . . . . . . . . . 14  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  ( [. ( y ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph )
)
166163, 165imbi12d 318 . . . . . . . . . . . . 13  |-  ( y  =  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  ->  (
( ( [. y  /  x ]. [. (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. )  /  w ]. ph  /\  ( # `  y )  =  (
# `  ( w substr  <.
0 ,  ( (
# `  w )  -  1 ) >.
) ) )  ->  [. ( y ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph )  <->  ( ( [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph )
) )
167 s1eq 12666 . . . . . . . . . . . . . . . 16  |-  ( z  =  ( lastS  `  x
)  ->  <" z ">  =  <" ( lastS  `  x ) "> )
168167oveq2d 6294 . . . . . . . . . . . . . . 15  |-  ( z  =  ( lastS  `  x
)  ->  ( (
x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" z "> )  =  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" ( lastS  `  x ) "> ) )
169168sbceq1d 3282 . . . . . . . . . . . . . 14  |-  ( z  =  ( lastS  `  x
)  ->  ( [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" ( lastS  `  x ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
170169imbi2d 314 . . . . . . . . . . . . 13  |-  ( z  =  ( lastS  `  x
)  ->  ( (
( [. ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" z "> )  /  x ]. [. ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  /  w ]. ph )  <->  ( ( [. ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
)  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" ( lastS  `  x ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
) )
171 simplr 754 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  (
y  e. Word  X  /\  z  e.  X )
)
172 simpll 752 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  (
u  e. Word  Y  /\  s  e.  Y )
)
173 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( # `
 y )  =  ( # `  u
) )
174 wrd2ind.7 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y  e. Word  X  /\  z  e.  X
)  /\  ( u  e. Word  Y  /\  s  e.  Y )  /\  ( # `
 y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
175171, 172, 173, 174syl3anc 1230 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( ch  ->  th ) )
17644ancoms 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  =  u  /\  x  =  y )  ->  ( ph  <->  ch )
)
177129, 128, 176sbc2ie 3345 . . . . . . . . . . . . . . . . 17  |-  ( [. u  /  w ]. [. y  /  x ]. ph  <->  ch )
178 ovex 6306 . . . . . . . . . . . . . . . . . 18  |-  ( u ++ 
<" s "> )  e.  _V
179 ovex 6306 . . . . . . . . . . . . . . . . . 18  |-  ( y ++ 
<" z "> )  e.  _V
180 wrd2ind.3 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  =  ( y ++ 
<" z "> )  /\  w  =  ( u ++  <" s "> ) )  -> 
( ph  <->  th ) )
181180ancoms 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  =  ( u ++ 
<" s "> )  /\  x  =  ( y ++  <" z "> ) )  -> 
( ph  <->  th ) )
182178, 179, 181sbc2ie 3345 . . . . . . . . . . . . . . . . 17  |-  ( [. ( u ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph  <->  th )
183175, 177, 1823imtr4g 270 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  /\  ( # `  y )  =  ( # `  u
) )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  ->  [. ( u ++ 
<" s "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph ) )
184183ex 432 . . . . . . . . . . . . . . 15  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( ( # `  y
)  =  ( # `  u )  ->  ( [. u  /  w ]. [. y  /  x ]. ph  ->  [. ( u ++ 
<" s "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph ) ) )
185184com23 78 . . . . . . . . . . . . . 14  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( [. u  /  w ]. [. y  /  x ]. ph  ->  ( ( # `
 y )  =  ( # `  u
)  ->  [. ( u ++ 
<" s "> )  /  w ]. [. (
y ++  <" z "> )  /  x ]. ph ) ) )
186185impd 429 . . . . . . . . . . . . 13  |-  ( ( ( u  e. Word  Y  /\  s  e.  Y
)  /\  ( y  e. Word  X  /\  z  e.  X ) )  -> 
( ( [. u  /  w ]. [. y  /  x ]. ph  /\  ( # `  y )  =  ( # `  u
) )  ->  [. (
u ++  <" s "> )  /  w ]. [. ( y ++  <" z "> )  /  x ]. ph )
)
187152, 160, 166, 170, 186vtocl4ga 3129 . . . . . . . . . . . 12  |-  ( ( ( ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  e. Word  Y  /\  ( lastS  `  w )  e.  Y )  /\  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. )  e. Word  X  /\  ( lastS  `  x )  e.  X ) )  ->  ( ( [. ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. )  /  x ]. [. ( w substr  <. 0 ,  ( ( # `  w )  -  1 ) >. )  /  w ]. ph  /\  ( # `  ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) )  =  ( # `  (
w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ) )  ->  [. ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" ( lastS  `  x ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
18884, 144, 187sylc 59 . . . . . . . . . . 11  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  [. (
( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" ( lastS  `  x ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
189 eqtr2 2429 . . . . . . . . . . . . . . . 16  |-  ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ( # `
 w )  =  ( m  +  1 ) )
190189ad2antll 727 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  =  ( m  +  1 ) )
191190, 92eqeltrd 2490 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( # `
 w )  e.  NN )
192 wrdfin 12613 . . . . . . . . . . . . . . . . 17  |-  ( w  e. Word  Y  ->  w  e.  Fin )
193192adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  w  e.  Fin )
194193ad2antrl 726 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  e.  Fin )
195 hashnncl 12484 . . . . . . . . . . . . . . 15  |-  ( w  e.  Fin  ->  (
( # `  w )  e.  NN  <->  w  =/=  (/) ) )
196194, 195syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  w )  e.  NN  <->  w  =/=  (/) ) )
197191, 196mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  =/=  (/) )
198 swrdccatwrd 12749 . . . . . . . . . . . . . 14  |-  ( ( w  e. Word  Y  /\  w  =/=  (/) )  ->  (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  =  w )
199198eqcomd 2410 . . . . . . . . . . . . 13  |-  ( ( w  e. Word  Y  /\  w  =/=  (/) )  ->  w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )
)
20099, 197, 199syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )
)
201 wrdfin 12613 . . . . . . . . . . . . . . . . 17  |-  ( x  e. Word  X  ->  x  e.  Fin )
202201adantl 464 . . . . . . . . . . . . . . . 16  |-  ( ( w  e. Word  Y  /\  x  e. Word  X )  ->  x  e.  Fin )
203202ad2antrl 726 . . . . . . . . . . . . . . 15  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  e.  Fin )
204 hashnncl 12484 . . . . . . . . . . . . . . 15  |-  ( x  e.  Fin  ->  (
( # `  x )  e.  NN  <->  x  =/=  (/) ) )
205203, 204syl 17 . . . . . . . . . . . . . 14  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  (
( # `  x )  e.  NN  <->  x  =/=  (/) ) )
20693, 205mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  =/=  (/) )
207 swrdccatwrd 12749 . . . . . . . . . . . . . 14  |-  ( ( x  e. Word  X  /\  x  =/=  (/) )  ->  (
( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" ( lastS  `  x ) "> )  =  x )
208207eqcomd 2410 . . . . . . . . . . . . 13  |-  ( ( x  e. Word  X  /\  x  =/=  (/) )  ->  x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) ++  <" ( lastS  `  x
) "> )
)
20989, 206, 208syl2anc 659 . . . . . . . . . . . 12  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) ++  <" ( lastS  `  x
) "> )
)
210 sbceq1a 3288 . . . . . . . . . . . . 13  |-  ( w  =  ( ( w substr  <. 0 ,  ( (
# `  w )  -  1 ) >.
) ++  <" ( lastS  `  w
) "> )  ->  ( ph  <->  [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
211 sbceq1a 3288 . . . . . . . . . . . . 13  |-  ( x  =  ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) ++  <" ( lastS  `  x
) "> )  ->  ( [. ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph  <->  [. ( ( x substr  <. 0 ,  ( ( # `  x
)  -  1 )
>. ) ++  <" ( lastS  `  x ) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
212210, 211sylan9bb 698 . . . . . . . . . . . 12  |-  ( ( w  =  ( ( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /\  x  =  ( ( x substr  <. 0 ,  ( ( # `  x )  -  1 ) >. ) ++  <" ( lastS  `  x ) "> ) )  ->  ( ph 
<-> 
[. ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) ++  <" ( lastS  `  x
) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
213200, 209, 212syl2anc 659 . . . . . . . . . . 11  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ( ph 
<-> 
[. ( ( x substr  <. 0 ,  ( (
# `  x )  -  1 ) >.
) ++  <" ( lastS  `  x
) "> )  /  x ]. [. (
( w substr  <. 0 ,  ( ( # `  w
)  -  1 )
>. ) ++  <" ( lastS  `  w ) "> )  /  w ]. ph )
)
214188, 213mpbird 232 . . . . . . . . . 10  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
( w  e. Word  Y  /\  x  e. Word  X )  /\  ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( m  +  1 ) ) ) )  ->  ph )
215214expr 613 . . . . . . . . 9  |-  ( ( ( m  e.  NN0  /\ 
A. u  e. Word  Y A. y  e. Word  X ( ( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  /\  (
w  e. Word  Y  /\  x  e. Word  X )
)  ->  ( (
( # `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) )
216215ralrimivva 2825 . . . . . . . 8  |-  ( ( m  e.  NN0  /\  A. u  e. Word  Y A. y  e. Word  X (
( ( # `  y
)  =  ( # `  u )  /\  ( # `
 y )  =  m )  ->  ch ) )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) )
217216ex 432 . . . . . . 7  |-  ( m  e.  NN0  ->  ( A. u  e. Word  Y A. y  e. Word  X ( ( (
# `  y )  =  ( # `  u
)  /\  ( # `  y
)  =  m )  ->  ch )  ->  A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( m  +  1 ) )  ->  ph )
) )
21848, 217syl5bi 217 . . . . . 6  |-  ( m  e.  NN0  ->  ( A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  m )  ->  ph )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( m  +  1 ) )  ->  ph ) ) )
2195, 9, 13, 17, 37, 218nn0ind 10998 . . . . 5  |-  ( (
# `  A )  e.  NN0  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
2201, 219syl 17 . . . 4  |-  ( A  e. Word  X  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
2212203ad2ant1 1018 . . 3  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  A. w  e. Word  Y A. x  e. Word  X ( ( (
# `  x )  =  ( # `  w
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph ) )
222 fveq2 5849 . . . . . . . . 9  |-  ( w  =  B  ->  ( # `
 w )  =  ( # `  B
) )
223222eqeq2d 2416 . . . . . . . 8  |-  ( w  =  B  ->  (
( # `  x )  =  ( # `  w
)  <->  ( # `  x
)  =  ( # `  B ) ) )
224223anbi1d 703 . . . . . . 7  |-  ( w  =  B  ->  (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  <->  ( ( # `
 x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) ) ) )
225 wrd2ind.5 . . . . . . 7  |-  ( w  =  B  ->  ( ph 
<->  rh ) )
226224, 225imbi12d 318 . . . . . 6  |-  ( w  =  B  ->  (
( ( ( # `  x )  =  (
# `  w )  /\  ( # `  x
)  =  ( # `  A ) )  ->  ph )  <->  ( ( (
# `  x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
227226ralbidv 2843 . . . . 5  |-  ( w  =  B  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  <->  A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh ) ) )
228227rspcv 3156 . . . 4  |-  ( B  e. Word  Y  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  ->  A. x  e. Word  X
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
2292283ad2ant2 1019 . . 3  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ( A. w  e. Word  Y A. x  e. Word  X (
( ( # `  x
)  =  ( # `  w )  /\  ( # `
 x )  =  ( # `  A
) )  ->  ph )  ->  A. x  e. Word  X
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) ) )
230221, 229mpd 15 . 2  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  A. x  e. Word  X ( ( (
# `  x )  =  ( # `  B
)  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh ) )
231 eqidd 2403 . 2  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ( # `
 A )  =  ( # `  A
) )
232 fveq2 5849 . . . . . . . . . . 11  |-  ( x  =  A  ->  ( # `
 x )  =  ( # `  A
) )
233232eqeq1d 2404 . . . . . . . . . 10  |-  ( x  =  A  ->  (
( # `  x )  =  ( # `  B
)  <->  ( # `  A
)  =  ( # `  B ) ) )
234232eqeq1d 2404 . . . . . . . . . 10  |-  ( x  =  A  ->  (
( # `  x )  =  ( # `  A
)  <->  ( # `  A
)  =  ( # `  A ) ) )
235233, 234anbi12d 709 . . . . . . . . 9  |-  ( x  =  A  ->  (
( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  <->  ( ( # `
 A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) ) ) )
236 wrd2ind.4 . . . . . . . . 9  |-  ( x  =  A  ->  ( rh 
<->  ta ) )
237235, 236imbi12d 318 . . . . . . . 8  |-  ( x  =  A  ->  (
( ( ( # `  x )  =  (
# `  B )  /\  ( # `  x
)  =  ( # `  A ) )  ->  rh )  <->  ( ( (
# `  A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) )  ->  ta ) ) )
238237rspcv 3156 . . . . . . 7  |-  ( A  e. Word  X  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ( ( (
# `  A )  =  ( # `  B
)  /\  ( # `  A
)  =  ( # `  A ) )  ->  ta ) ) )
239238com23 78 . . . . . 6  |-  ( A  e. Word  X  ->  (
( ( # `  A
)  =  ( # `  B )  /\  ( # `
 A )  =  ( # `  A
) )  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ta ) ) )
240239expd 434 . . . . 5  |-  ( A  e. Word  X  ->  (
( # `  A )  =  ( # `  B
)  ->  ( ( # `
 A )  =  ( # `  A
)  ->  ( A. x  e. Word  X (
( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ta ) ) ) )
241240com34 83 . . . 4  |-  ( A  e. Word  X  ->  (
( # `  A )  =  ( # `  B
)  ->  ( A. x  e. Word  X (
( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ( ( # `  A )  =  (
# `  A )  ->  ta ) ) ) )
242241imp 427 . . 3  |-  ( ( A  e. Word  X  /\  ( # `  A )  =  ( # `  B
) )  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ( ( # `  A )  =  (
# `  A )  ->  ta ) ) )
2432423adant2 1016 . 2  |-  ( ( A  e. Word  X  /\  B  e. Word  Y  /\  ( # `
 A )  =  ( # `  B
) )  ->  ( A. x  e. Word  X ( ( ( # `  x
)  =  ( # `  B )  /\  ( # `
 x )  =  ( # `  A
) )  ->  rh )  ->  ( ( # `  A )  =  (
# `  A )  ->  ta ) ) )
244