Metamath Proof Explorer

Theorem ccatswrd

Description: Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015)

Ref Expression
Assertion ccatswrd 
|- ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) = ( S substr <. X , Z >. ) )

Proof

Step Hyp Ref Expression
1 swrdcl 
 |-  ( S e. Word A -> ( S substr <. X , Y >. ) e. Word A )
2 1 adantr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. X , Y >. ) e. Word A )
3 swrdcl 
 |-  ( S e. Word A -> ( S substr <. Y , Z >. ) e. Word A )
4 3 adantr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. Y , Z >. ) e. Word A )
5 ccatcl 
 |-  ( ( ( S substr <. X , Y >. ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) e. Word A )
6 2 4 5 syl2anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) e. Word A )
7 wrdfn 
 |-  ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) e. Word A -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) ) )
8 6 7 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) ) )
9 ccatlen 
 |-  ( ( ( S substr <. X , Y >. ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A ) -> ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) = ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) )
10 2 4 9 syl2anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) = ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) )
11 simpl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> S e. Word A )
12 simpr1 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. ( 0 ... Y ) )
13 simpr2 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ( 0 ... Z ) )
14 simpr3 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Z e. ( 0 ... ( # ` S ) ) )
15 fzass4 
 |-  ( ( Y e. ( 0 ... ( # ` S ) ) /\ Z e. ( Y ... ( # ` S ) ) ) <-> ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) )
16 15 biimpri 
 |-  ( ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( Y e. ( 0 ... ( # ` S ) ) /\ Z e. ( Y ... ( # ` S ) ) ) )
17 16 simpld 
 |-  ( ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
18 13 14 17 syl2anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
19 swrdlen 
 |-  ( ( S e. Word A /\ X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. X , Y >. ) ) = ( Y - X ) )
20 11 12 18 19 syl3anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S substr <. X , Y >. ) ) = ( Y - X ) )
21 swrdlen 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. Y , Z >. ) ) = ( Z - Y ) )
22 21 3adant3r1 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S substr <. Y , Z >. ) ) = ( Z - Y ) )
23 20 22 oveq12d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) = ( ( Y - X ) + ( Z - Y ) ) )
24 elfzelz 
 |-  ( Y e. ( 0 ... Z ) -> Y e. ZZ )
25 13 24 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ZZ )
26 25 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. CC )
27 elfzelz 
 |-  ( X e. ( 0 ... Y ) -> X e. ZZ )
28 12 27 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. ZZ )
29 28 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. CC )
30 elfzelz 
 |-  ( Z e. ( 0 ... ( # ` S ) ) -> Z e. ZZ )
31 14 30 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Z e. ZZ )
32 31 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Z e. CC )
33 26 29 32 npncan3d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( Y - X ) + ( Z - Y ) ) = ( Z - X ) )
34 10 23 33 3eqtrd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) = ( Z - X ) )
35 34 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( 0 ..^ ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) ) = ( 0 ..^ ( Z - X ) ) )
36 35 fneq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ) ) <-> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( Z - X ) ) ) )
37 8 36 mpbid 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( Z - X ) ) )
38 swrdcl 
 |-  ( S e. Word A -> ( S substr <. X , Z >. ) e. Word A )
39 38 adantr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. X , Z >. ) e. Word A )
40 wrdfn 
 |-  ( ( S substr <. X , Z >. ) e. Word A -> ( S substr <. X , Z >. ) Fn ( 0 ..^ ( # ` ( S substr <. X , Z >. ) ) ) )
41 39 40 syl 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. X , Z >. ) Fn ( 0 ..^ ( # ` ( S substr <. X , Z >. ) ) ) )
42 fzass4 
 |-  ( ( X e. ( 0 ... Z ) /\ Y e. ( X ... Z ) ) <-> ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) )
43 42 biimpri 
 |-  ( ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) -> ( X e. ( 0 ... Z ) /\ Y e. ( X ... Z ) ) )
44 43 simpld 
 |-  ( ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) -> X e. ( 0 ... Z ) )
45 12 13 44 syl2anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. ( 0 ... Z ) )
46 swrdlen 
 |-  ( ( S e. Word A /\ X e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. X , Z >. ) ) = ( Z - X ) )
47 11 45 14 46 syl3anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S substr <. X , Z >. ) ) = ( Z - X ) )
48 47 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( 0 ..^ ( # ` ( S substr <. X , Z >. ) ) ) = ( 0 ..^ ( Z - X ) ) )
49 48 fneq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Z >. ) Fn ( 0 ..^ ( # ` ( S substr <. X , Z >. ) ) ) <-> ( S substr <. X , Z >. ) Fn ( 0 ..^ ( Z - X ) ) ) )
50 41 49 mpbid 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. X , Z >. ) Fn ( 0 ..^ ( Z - X ) ) )
51 25 28 zsubcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - X ) e. ZZ )
52 51 anim1ci 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( x e. ( 0 ..^ ( Z - X ) ) /\ ( Y - X ) e. ZZ ) )
53 fzospliti 
 |-  ( ( x e. ( 0 ..^ ( Z - X ) ) /\ ( Y - X ) e. ZZ ) -> ( x e. ( 0 ..^ ( Y - X ) ) \/ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) )
54 52 53 syl 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( x e. ( 0 ..^ ( Y - X ) ) \/ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) )
55 1 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( S substr <. X , Y >. ) e. Word A )
56 3 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( S substr <. Y , Z >. ) e. Word A )
57 20 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( 0 ..^ ( # ` ( S substr <. X , Y >. ) ) ) = ( 0 ..^ ( Y - X ) ) )
58 57 eleq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( 0 ..^ ( # ` ( S substr <. X , Y >. ) ) ) <-> x e. ( 0 ..^ ( Y - X ) ) ) )
59 58 biimpar 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> x e. ( 0 ..^ ( # ` ( S substr <. X , Y >. ) ) ) )
60 ccatval1 
 |-  ( ( ( S substr <. X , Y >. ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A /\ x e. ( 0 ..^ ( # ` ( S substr <. X , Y >. ) ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. X , Y >. ) ` x ) )
61 55 56 59 60 syl3anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. X , Y >. ) ` x ) )
62 simpll 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> S e. Word A )
63 simplr1 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> X e. ( 0 ... Y ) )
64 18 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
65 simpr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> x e. ( 0 ..^ ( Y - X ) ) )
66 swrdfv 
 |-  ( ( ( S e. Word A /\ X e. ( 0 ... Y ) /\ Y e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( ( S substr <. X , Y >. ) ` x ) = ( S ` ( x + X ) ) )
67 62 63 64 65 66 syl31anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( ( S substr <. X , Y >. ) ` x ) = ( S ` ( x + X ) ) )
68 61 67 eqtrd 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Y - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` ( x + X ) ) )
69 1 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( S substr <. X , Y >. ) e. Word A )
70 3 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( S substr <. Y , Z >. ) e. Word A )
71 23 33 eqtrd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) = ( Z - X ) )
72 20 71 oveq12d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S substr <. X , Y >. ) ) ..^ ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) = ( ( Y - X ) ..^ ( Z - X ) ) )
73 72 eleq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( ( # ` ( S substr <. X , Y >. ) ) ..^ ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) <-> x e. ( ( Y - X ) ..^ ( Z - X ) ) ) )
74 73 biimpar 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> x e. ( ( # ` ( S substr <. X , Y >. ) ) ..^ ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) )
75 ccatval2 
 |-  ( ( ( S substr <. X , Y >. ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A /\ x e. ( ( # ` ( S substr <. X , Y >. ) ) ..^ ( ( # ` ( S substr <. X , Y >. ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S substr <. X , Y >. ) ) ) ) )
76 69 70 74 75 syl3anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S substr <. X , Y >. ) ) ) ) )
77 simpll 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> S e. Word A )
78 simplr2 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> Y e. ( 0 ... Z ) )
79 simplr3 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> Z e. ( 0 ... ( # ` S ) ) )
80 20 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x - ( # ` ( S substr <. X , Y >. ) ) ) = ( x - ( Y - X ) ) )
81 80 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( x - ( # ` ( S substr <. X , Y >. ) ) ) = ( x - ( Y - X ) ) )
82 33 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( Y - X ) ..^ ( ( Y - X ) + ( Z - Y ) ) ) = ( ( Y - X ) ..^ ( Z - X ) ) )
83 82 eleq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( ( Y - X ) ..^ ( ( Y - X ) + ( Z - Y ) ) ) <-> x e. ( ( Y - X ) ..^ ( Z - X ) ) ) )
84 83 biimpar 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> x e. ( ( Y - X ) ..^ ( ( Y - X ) + ( Z - Y ) ) ) )
85 31 25 zsubcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Z - Y ) e. ZZ )
86 85 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( Z - Y ) e. ZZ )
87 fzosubel3 
 |-  ( ( x e. ( ( Y - X ) ..^ ( ( Y - X ) + ( Z - Y ) ) ) /\ ( Z - Y ) e. ZZ ) -> ( x - ( Y - X ) ) e. ( 0 ..^ ( Z - Y ) ) )
88 84 86 87 syl2anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( x - ( Y - X ) ) e. ( 0 ..^ ( Z - Y ) ) )
89 81 88 eqeltrd 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( x - ( # ` ( S substr <. X , Y >. ) ) ) e. ( 0 ..^ ( Z - Y ) ) )
90 swrdfv 
 |-  ( ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) /\ ( x - ( # ` ( S substr <. X , Y >. ) ) ) e. ( 0 ..^ ( Z - Y ) ) ) -> ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S substr <. X , Y >. ) ) ) ) = ( S ` ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) ) )
91 77 78 79 89 90 syl31anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S substr <. X , Y >. ) ) ) ) = ( S ` ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) ) )
92 80 oveq1d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) = ( ( x - ( Y - X ) ) + Y ) )
93 92 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) = ( ( x - ( Y - X ) ) + Y ) )
94 elfzoelz 
 |-  ( x e. ( ( Y - X ) ..^ ( Z - X ) ) -> x e. ZZ )
95 94 zcnd 
 |-  ( x e. ( ( Y - X ) ..^ ( Z - X ) ) -> x e. CC )
96 95 adantl 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> x e. CC )
97 26 29 subcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - X ) e. CC )
98 97 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( Y - X ) e. CC )
99 26 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> Y e. CC )
100 96 98 99 subadd23d 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( x - ( Y - X ) ) + Y ) = ( x + ( Y - ( Y - X ) ) ) )
101 26 29 nncand 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - ( Y - X ) ) = X )
102 101 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x + ( Y - ( Y - X ) ) ) = ( x + X ) )
103 102 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( x + ( Y - ( Y - X ) ) ) = ( x + X ) )
104 93 100 103 3eqtrd 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) = ( x + X ) )
105 104 fveq2d 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( S ` ( ( x - ( # ` ( S substr <. X , Y >. ) ) ) + Y ) ) = ( S ` ( x + X ) ) )
106 76 91 105 3eqtrd 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` ( x + X ) ) )
107 68 106 jaodan 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ ( x e. ( 0 ..^ ( Y - X ) ) \/ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` ( x + X ) ) )
108 54 107 syldan 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` ( x + X ) ) )
109 simpll 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> S e. Word A )
110 45 adantr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> X e. ( 0 ... Z ) )
111 simplr3 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> Z e. ( 0 ... ( # ` S ) ) )
112 simpr 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> x e. ( 0 ..^ ( Z - X ) ) )
113 swrdfv 
 |-  ( ( ( S e. Word A /\ X e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( ( S substr <. X , Z >. ) ` x ) = ( S ` ( x + X ) ) )
114 109 110 111 112 113 syl31anc 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( ( S substr <. X , Z >. ) ` x ) = ( S ` ( x + X ) ) )
115 108 114 eqtr4d 
 |-  ( ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ ( Z - X ) ) ) -> ( ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. X , Z >. ) ` x ) )
116 37 50 115 eqfnfvd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S substr <. X , Y >. ) ++ ( S substr <. Y , Z >. ) ) = ( S substr <. X , Z >. ) )