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 13 elfzelzd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ZZ )
25 24 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. CC )
26 12 elfzelzd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. ZZ )
27 26 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. CC )
28 14 elfzelzd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Z e. ZZ )
29 28 zcnd 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Z e. CC )
30 25 27 29 npncan3d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( Y - X ) + ( Z - Y ) ) = ( Z - X ) )
31 10 23 30 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 ) )
32 31 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 ) ) )
33 32 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 ) ) ) )
34 8 33 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 ) ) )
35 swrdcl 
 |-  ( S e. Word A -> ( S substr <. X , Z >. ) e. Word A )
36 35 adantr 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S substr <. X , Z >. ) e. Word A )
37 wrdfn 
 |-  ( ( S substr <. X , Z >. ) e. Word A -> ( S substr <. X , Z >. ) Fn ( 0 ..^ ( # ` ( S substr <. X , Z >. ) ) ) )
38 36 37 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 >. ) ) ) )
39 fzass4 
 |-  ( ( X e. ( 0 ... Z ) /\ Y e. ( X ... Z ) ) <-> ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) )
40 39 biimpri 
 |-  ( ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) -> ( X e. ( 0 ... Z ) /\ Y e. ( X ... Z ) ) )
41 40 simpld 
 |-  ( ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) ) -> X e. ( 0 ... Z ) )
42 12 13 41 syl2anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> X e. ( 0 ... Z ) )
43 swrdlen 
 |-  ( ( S e. Word A /\ X e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. X , Z >. ) ) = ( Z - X ) )
44 11 42 14 43 syl3anc 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S substr <. X , Z >. ) ) = ( Z - X ) )
45 44 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 ) ) )
46 45 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 ) ) ) )
47 38 46 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 ) ) )
48 24 26 zsubcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - X ) e. ZZ )
49 48 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 ) )
50 fzospliti 
 |-  ( ( x e. ( 0 ..^ ( Z - X ) ) /\ ( Y - X ) e. ZZ ) -> ( x e. ( 0 ..^ ( Y - X ) ) \/ x e. ( ( Y - X ) ..^ ( Z - X ) ) ) )
51 49 50 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 ) ) ) )
52 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 )
53 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 )
54 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 ) ) )
55 54 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 ) ) ) )
56 55 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 >. ) ) ) )
57 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 ) )
58 52 53 56 57 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 ) )
59 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 )
60 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 ) )
61 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 ) ) )
62 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 ) ) )
63 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 ) ) )
64 59 60 61 62 63 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 ) ) )
65 58 64 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 ) ) )
66 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 )
67 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 )
68 23 30 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 ) )
69 20 68 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 ) ) )
70 69 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 ) ) ) )
71 70 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 >. ) ) ) ) )
72 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 >. ) ) ) ) )
73 66 67 71 72 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 >. ) ) ) ) )
74 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 )
75 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 ) )
76 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 ) ) )
77 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 ) ) )
78 77 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 ) ) )
79 30 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 ) ) )
80 79 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 ) ) ) )
81 80 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 ) ) ) )
82 28 24 zsubcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Z - Y ) e. ZZ )
83 82 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 )
84 fzosubel3 
 |-  ( ( x e. ( ( Y - X ) ..^ ( ( Y - X ) + ( Z - Y ) ) ) /\ ( Z - Y ) e. ZZ ) -> ( x - ( Y - X ) ) e. ( 0 ..^ ( Z - Y ) ) )
85 81 83 84 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 ) ) )
86 78 85 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 ) ) )
87 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 ) ) )
88 74 75 76 86 87 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 ) ) )
89 77 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 ) )
90 89 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 ) )
91 elfzoelz 
 |-  ( x e. ( ( Y - X ) ..^ ( Z - X ) ) -> x e. ZZ )
92 91 zcnd 
 |-  ( x e. ( ( Y - X ) ..^ ( Z - X ) ) -> x e. CC )
93 92 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 )
94 25 27 subcld 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - X ) e. CC )
95 94 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 )
96 25 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 )
97 93 95 96 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 ) ) ) )
98 25 27 nncand 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y - ( Y - X ) ) = X )
99 98 oveq2d 
 |-  ( ( S e. Word A /\ ( X e. ( 0 ... Y ) /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x + ( Y - ( Y - X ) ) ) = ( x + X ) )
100 99 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 ) )
101 90 97 100 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 ) )
102 101 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 ) ) )
103 73 88 102 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 ) ) )
104 65 103 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 ) ) )
105 51 104 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 ) ) )
106 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 )
107 42 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 ) )
108 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 ) ) )
109 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 ) ) )
110 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 ) ) )
111 106 107 108 109 110 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 ) ) )
112 105 111 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 ) )
113 34 47 112 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 >. ) )