Metamath Proof Explorer

Theorem ccatpfx

Description: Concatenating a prefix with an adjacent subword makes a longer prefix. (Contributed by AV, 7-May-2020)

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

Proof

Step Hyp Ref Expression
1 pfxcl 
 |-  ( S e. Word A -> ( S prefix Y ) e. Word A )
2 swrdcl 
 |-  ( S e. Word A -> ( S substr <. Y , Z >. ) e. Word A )
3 ccatcl 
 |-  ( ( ( S prefix Y ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) e. Word A )
4 1 2 3 syl2anc 
 |-  ( S e. Word A -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) e. Word A )
5 wrdfn 
 |-  ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) e. Word A -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) ) )
6 4 5 syl 
 |-  ( S e. Word A -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) ) )
7 6 adantr 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) ) )
8 ccatlen 
 |-  ( ( ( S prefix Y ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A ) -> ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) = ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) )
9 1 2 8 syl2anc 
 |-  ( S e. Word A -> ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) = ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) )
10 9 adantr 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) = ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) )
11 fzass4 
 |-  ( ( Y e. ( 0 ... ( # ` S ) ) /\ Z e. ( Y ... ( # ` S ) ) ) <-> ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) )
12 11 biimpri 
 |-  ( ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( Y e. ( 0 ... ( # ` S ) ) /\ Z e. ( Y ... ( # ` S ) ) ) )
13 12 simpld 
 |-  ( ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
14 pfxlen 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S prefix Y ) ) = Y )
15 13 14 sylan2 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S prefix Y ) ) = Y )
16 swrdlen 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( # ` ( S substr <. Y , Z >. ) ) = ( Z - Y ) )
17 16 3expb 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( S substr <. Y , Z >. ) ) = ( Z - Y ) )
18 15 17 oveq12d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) = ( Y + ( Z - Y ) ) )
19 elfzelz 
 |-  ( Y e. ( 0 ... Z ) -> Y e. ZZ )
20 19 zcnd 
 |-  ( Y e. ( 0 ... Z ) -> Y e. CC )
21 elfzelz 
 |-  ( Z e. ( 0 ... ( # ` S ) ) -> Z e. ZZ )
22 21 zcnd 
 |-  ( Z e. ( 0 ... ( # ` S ) ) -> Z e. CC )
23 pncan3 
 |-  ( ( Y e. CC /\ Z e. CC ) -> ( Y + ( Z - Y ) ) = Z )
24 20 22 23 syl2an 
 |-  ( ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( Y + ( Z - Y ) ) = Z )
25 24 adantl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( Y + ( Z - Y ) ) = Z )
26 10 18 25 3eqtrd 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) = Z )
27 26 oveq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( 0 ..^ ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) ) = ( 0 ..^ Z ) )
28 27 fneq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ ( # ` ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ) ) <-> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ Z ) ) )
29 7 28 mpbid 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) Fn ( 0 ..^ Z ) )
30 pfxfn 
 |-  ( ( S e. Word A /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( S prefix Z ) Fn ( 0 ..^ Z ) )
31 30 adantrl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S prefix Z ) Fn ( 0 ..^ Z ) )
32 id 
 |-  ( x e. ( 0 ..^ Z ) -> x e. ( 0 ..^ Z ) )
33 19 ad2antrl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ZZ )
34 fzospliti 
 |-  ( ( x e. ( 0 ..^ Z ) /\ Y e. ZZ ) -> ( x e. ( 0 ..^ Y ) \/ x e. ( Y ..^ Z ) ) )
35 32 33 34 syl2anr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Z ) ) -> ( x e. ( 0 ..^ Y ) \/ x e. ( Y ..^ Z ) ) )
36 1 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> ( S prefix Y ) e. Word A )
37 2 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> ( S substr <. Y , Z >. ) e. Word A )
38 15 oveq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( 0 ..^ ( # ` ( S prefix Y ) ) ) = ( 0 ..^ Y ) )
39 38 eleq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( 0 ..^ ( # ` ( S prefix Y ) ) ) <-> x e. ( 0 ..^ Y ) ) )
40 39 biimpar 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> x e. ( 0 ..^ ( # ` ( S prefix Y ) ) ) )
41 ccatval1 
 |-  ( ( ( S prefix Y ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A /\ x e. ( 0 ..^ ( # ` ( S prefix Y ) ) ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S prefix Y ) ` x ) )
42 36 37 40 41 syl3anc 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S prefix Y ) ` x ) )
43 simpl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> S e. Word A )
44 13 adantl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. ( 0 ... ( # ` S ) ) )
45 id 
 |-  ( x e. ( 0 ..^ Y ) -> x e. ( 0 ..^ Y ) )
46 pfxfv 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... ( # ` S ) ) /\ x e. ( 0 ..^ Y ) ) -> ( ( S prefix Y ) ` x ) = ( S ` x ) )
47 43 44 45 46 syl2an3an 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> ( ( S prefix Y ) ` x ) = ( S ` x ) )
48 42 47 eqtrd 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Y ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` x ) )
49 1 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( S prefix Y ) e. Word A )
50 2 ad2antrr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( S substr <. Y , Z >. ) e. Word A )
51 18 25 eqtrd 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) = Z )
52 15 51 oveq12d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( # ` ( S prefix Y ) ) ..^ ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) = ( Y ..^ Z ) )
53 52 eleq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x e. ( ( # ` ( S prefix Y ) ) ..^ ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) <-> x e. ( Y ..^ Z ) ) )
54 53 biimpar 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> x e. ( ( # ` ( S prefix Y ) ) ..^ ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) )
55 ccatval2 
 |-  ( ( ( S prefix Y ) e. Word A /\ ( S substr <. Y , Z >. ) e. Word A /\ x e. ( ( # ` ( S prefix Y ) ) ..^ ( ( # ` ( S prefix Y ) ) + ( # ` ( S substr <. Y , Z >. ) ) ) ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S prefix Y ) ) ) ) )
56 49 50 54 55 syl3anc 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S prefix Y ) ) ) ) )
57 id 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) )
58 57 3expb 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) )
59 15 oveq2d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( x - ( # ` ( S prefix Y ) ) ) = ( x - Y ) )
60 59 adantr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( x - ( # ` ( S prefix Y ) ) ) = ( x - Y ) )
61 id 
 |-  ( x e. ( Y ..^ Z ) -> x e. ( Y ..^ Z ) )
62 fzosubel 
 |-  ( ( x e. ( Y ..^ Z ) /\ Y e. ZZ ) -> ( x - Y ) e. ( ( Y - Y ) ..^ ( Z - Y ) ) )
63 61 33 62 syl2anr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( x - Y ) e. ( ( Y - Y ) ..^ ( Z - Y ) ) )
64 20 subidd 
 |-  ( Y e. ( 0 ... Z ) -> ( Y - Y ) = 0 )
65 64 oveq1d 
 |-  ( Y e. ( 0 ... Z ) -> ( ( Y - Y ) ..^ ( Z - Y ) ) = ( 0 ..^ ( Z - Y ) ) )
66 65 eleq2d 
 |-  ( Y e. ( 0 ... Z ) -> ( ( x - Y ) e. ( ( Y - Y ) ..^ ( Z - Y ) ) <-> ( x - Y ) e. ( 0 ..^ ( Z - Y ) ) ) )
67 66 ad2antrl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( x - Y ) e. ( ( Y - Y ) ..^ ( Z - Y ) ) <-> ( x - Y ) e. ( 0 ..^ ( Z - Y ) ) ) )
68 67 adantr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( x - Y ) e. ( ( Y - Y ) ..^ ( Z - Y ) ) <-> ( x - Y ) e. ( 0 ..^ ( Z - Y ) ) ) )
69 63 68 mpbid 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( x - Y ) e. ( 0 ..^ ( Z - Y ) ) )
70 60 69 eqeltrd 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( x - ( # ` ( S prefix Y ) ) ) e. ( 0 ..^ ( Z - Y ) ) )
71 swrdfv 
 |-  ( ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) /\ ( x - ( # ` ( S prefix Y ) ) ) e. ( 0 ..^ ( Z - Y ) ) ) -> ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S prefix Y ) ) ) ) = ( S ` ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) ) )
72 58 70 71 syl2an2r 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( S substr <. Y , Z >. ) ` ( x - ( # ` ( S prefix Y ) ) ) ) = ( S ` ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) ) )
73 59 oveq1d 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) = ( ( x - Y ) + Y ) )
74 73 adantr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) = ( ( x - Y ) + Y ) )
75 elfzoelz 
 |-  ( x e. ( Y ..^ Z ) -> x e. ZZ )
76 75 zcnd 
 |-  ( x e. ( Y ..^ Z ) -> x e. CC )
77 20 ad2antrl 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> Y e. CC )
78 npcan 
 |-  ( ( x e. CC /\ Y e. CC ) -> ( ( x - Y ) + Y ) = x )
79 76 77 78 syl2anr 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( x - Y ) + Y ) = x )
80 74 79 eqtrd 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) = x )
81 80 fveq2d 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( S ` ( ( x - ( # ` ( S prefix Y ) ) ) + Y ) ) = ( S ` x ) )
82 56 72 81 3eqtrd 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( Y ..^ Z ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` x ) )
83 48 82 jaodan 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ ( x e. ( 0 ..^ Y ) \/ x e. ( Y ..^ Z ) ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` x ) )
84 35 83 syldan 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Z ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( S ` x ) )
85 pfxfv 
 |-  ( ( S e. Word A /\ Z e. ( 0 ... ( # ` S ) ) /\ x e. ( 0 ..^ Z ) ) -> ( ( S prefix Z ) ` x ) = ( S ` x ) )
86 85 3expa 
 |-  ( ( ( S e. Word A /\ Z e. ( 0 ... ( # ` S ) ) ) /\ x e. ( 0 ..^ Z ) ) -> ( ( S prefix Z ) ` x ) = ( S ` x ) )
87 86 adantlrl 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Z ) ) -> ( ( S prefix Z ) ` x ) = ( S ` x ) )
88 84 87 eqtr4d 
 |-  ( ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) /\ x e. ( 0 ..^ Z ) ) -> ( ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) ` x ) = ( ( S prefix Z ) ` x ) )
89 29 31 88 eqfnfvd 
 |-  ( ( S e. Word A /\ ( Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) = ( S prefix Z ) )
90 89 3impb 
 |-  ( ( S e. Word A /\ Y e. ( 0 ... Z ) /\ Z e. ( 0 ... ( # ` S ) ) ) -> ( ( S prefix Y ) ++ ( S substr <. Y , Z >. ) ) = ( S prefix Z ) )