This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pfxccatin12

Description: The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018) (Revised by AV, 9-May-2020)

Ref Expression
Hypothesis swrdccatin2.l 
|- L = ( # ` A )
Assertion pfxccatin12 
|- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 1 pfxccatin12lem2c 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
3 swrdvalfn 
 |-  ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
4 2 3 syl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
5 swrdcl 
 |-  ( A e. Word V -> ( A substr <. M , L >. ) e. Word V )
6 pfxcl 
 |-  ( B e. Word V -> ( B prefix ( N - L ) ) e. Word V )
7 ccatvalfn 
 |-  ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) -> ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) )
8 5 6 7 syl2an 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) )
9 8 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) )
10 simpll 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> A e. Word V )
11 simprl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> M e. ( 0 ... L ) )
12 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
13 nn0fz0 
 |-  ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
14 12 13 sylib 
 |-  ( A e. Word V -> ( # ` A ) e. ( 0 ... ( # ` A ) ) )
15 1 14 eqeltrid 
 |-  ( A e. Word V -> L e. ( 0 ... ( # ` A ) ) )
16 15 ad2antrr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> L e. ( 0 ... ( # ` A ) ) )
17 swrdlen 
 |-  ( ( A e. Word V /\ M e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` A ) ) ) -> ( # ` ( A substr <. M , L >. ) ) = ( L - M ) )
18 10 11 16 17 syl3anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( # ` ( A substr <. M , L >. ) ) = ( L - M ) )
19 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
20 19 nn0zd 
 |-  ( B e. Word V -> ( # ` B ) e. ZZ )
21 elfzmlbp 
 |-  ( ( ( # ` B ) e. ZZ /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
22 20 21 sylan 
 |-  ( ( B e. Word V /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
23 pfxlen 
 |-  ( ( B e. Word V /\ ( N - L ) e. ( 0 ... ( # ` B ) ) ) -> ( # ` ( B prefix ( N - L ) ) ) = ( N - L ) )
24 22 23 syldan 
 |-  ( ( B e. Word V /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( # ` ( B prefix ( N - L ) ) ) = ( N - L ) )
25 24 ad2ant2l 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( # ` ( B prefix ( N - L ) ) ) = ( N - L ) )
26 18 25 oveq12d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) = ( ( L - M ) + ( N - L ) ) )
27 elfz2nn0 
 |-  ( M e. ( 0 ... L ) <-> ( M e. NN0 /\ L e. NN0 /\ M <_ L ) )
28 nn0cn 
 |-  ( L e. NN0 -> L e. CC )
29 28 ad2antll 
 |-  ( ( N e. ZZ /\ ( M e. NN0 /\ L e. NN0 ) ) -> L e. CC )
30 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
31 30 ad2antrl 
 |-  ( ( N e. ZZ /\ ( M e. NN0 /\ L e. NN0 ) ) -> M e. CC )
32 zcn 
 |-  ( N e. ZZ -> N e. CC )
33 32 adantr 
 |-  ( ( N e. ZZ /\ ( M e. NN0 /\ L e. NN0 ) ) -> N e. CC )
34 29 31 33 3jca 
 |-  ( ( N e. ZZ /\ ( M e. NN0 /\ L e. NN0 ) ) -> ( L e. CC /\ M e. CC /\ N e. CC ) )
35 34 ex 
 |-  ( N e. ZZ -> ( ( M e. NN0 /\ L e. NN0 ) -> ( L e. CC /\ M e. CC /\ N e. CC ) ) )
36 elfzelz 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) -> N e. ZZ )
37 35 36 syl11 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( L e. CC /\ M e. CC /\ N e. CC ) ) )
38 37 3adant3 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( L e. CC /\ M e. CC /\ N e. CC ) ) )
39 27 38 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( L e. CC /\ M e. CC /\ N e. CC ) ) )
40 39 imp 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( L e. CC /\ M e. CC /\ N e. CC ) )
41 npncan3 
 |-  ( ( L e. CC /\ M e. CC /\ N e. CC ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
42 40 41 syl 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
43 42 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( L - M ) + ( N - L ) ) = ( N - M ) )
44 26 43 eqtr2d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( N - M ) = ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) )
45 44 oveq2d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( 0 ..^ ( N - M ) ) = ( 0 ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) )
46 45 fneq2d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( N - M ) ) <-> ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) ) )
47 9 46 mpbird 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) Fn ( 0 ..^ ( N - M ) ) )
48 simprl 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
49 simpr 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> k e. ( 0 ..^ ( N - M ) ) )
50 49 anim2i 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( k e. ( 0 ..^ ( L - M ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) )
51 50 ancomd 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( k e. ( 0 ..^ ( N - M ) ) /\ k e. ( 0 ..^ ( L - M ) ) ) )
52 1 pfxccatin12lem3 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( k e. ( 0 ..^ ( N - M ) ) /\ k e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A substr <. M , L >. ) ` k ) ) )
53 48 51 52 sylc 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A substr <. M , L >. ) ` k ) )
54 5 6 anim12i 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) )
55 54 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) )
56 55 ad2antrl 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) )
57 simpl 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> k e. ( 0 ..^ ( L - M ) ) )
58 18 oveq2d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) = ( 0 ..^ ( L - M ) ) )
59 58 ad2antrl 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) = ( 0 ..^ ( L - M ) ) )
60 57 59 eleqtrrd 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> k e. ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) )
61 df-3an 
 |-  ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) ) <-> ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) /\ k e. ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) ) )
62 56 60 61 sylanbrc 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) ) )
63 ccatval1 
 |-  ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( 0 ..^ ( # ` ( A substr <. M , L >. ) ) ) ) -> ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) = ( ( A substr <. M , L >. ) ` k ) )
64 62 63 syl 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) = ( ( A substr <. M , L >. ) ` k ) )
65 53 64 eqtr4d 
 |-  ( ( k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) )
66 simprl 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) )
67 49 anim2i 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( -. k e. ( 0 ..^ ( L - M ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) )
68 67 ancomd 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( k e. ( 0 ..^ ( N - M ) ) /\ -. k e. ( 0 ..^ ( L - M ) ) ) )
69 1 pfxccatin12lem2 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( k e. ( 0 ..^ ( N - M ) ) /\ -. k e. ( 0 ..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( B prefix ( N - L ) ) ` ( k - ( # ` ( A substr <. M , L >. ) ) ) ) ) )
70 66 68 69 sylc 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( B prefix ( N - L ) ) ` ( k - ( # ` ( A substr <. M , L >. ) ) ) ) )
71 55 ad2antrl 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) )
72 elfzuz 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) -> N e. ( ZZ>= ` L ) )
73 eluzelz 
 |-  ( N e. ( ZZ>= ` L ) -> N e. ZZ )
74 id 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) )
75 74 3expia 
 |-  ( ( L e. NN0 /\ M e. NN0 ) -> ( N e. ZZ -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
76 75 ancoms 
 |-  ( ( M e. NN0 /\ L e. NN0 ) -> ( N e. ZZ -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
77 76 3adant3 
 |-  ( ( M e. NN0 /\ L e. NN0 /\ M <_ L ) -> ( N e. ZZ -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
78 27 77 sylbi 
 |-  ( M e. ( 0 ... L ) -> ( N e. ZZ -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
79 73 78 syl5com 
 |-  ( N e. ( ZZ>= ` L ) -> ( M e. ( 0 ... L ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
80 72 79 syl 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( M e. ( 0 ... L ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) ) )
81 80 impcom 
 |-  ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) )
82 81 adantl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) )
83 82 ad2antrl 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) )
84 pfxccatin12lem4 
 |-  ( ( L e. NN0 /\ M e. NN0 /\ N e. ZZ ) -> ( ( k e. ( 0 ..^ ( N - M ) ) /\ -. k e. ( 0 ..^ ( L - M ) ) ) -> k e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) ) )
85 83 68 84 sylc 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> k e. ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) )
86 18 26 oveq12d 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) = ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) )
87 86 ad2antrl 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) = ( ( L - M ) ..^ ( ( L - M ) + ( N - L ) ) ) )
88 85 87 eleqtrrd 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> k e. ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) )
89 df-3an 
 |-  ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) ) <-> ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V ) /\ k e. ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) ) )
90 71 88 89 sylanbrc 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) ) )
91 ccatval2 
 |-  ( ( ( A substr <. M , L >. ) e. Word V /\ ( B prefix ( N - L ) ) e. Word V /\ k e. ( ( # ` ( A substr <. M , L >. ) ) ..^ ( ( # ` ( A substr <. M , L >. ) ) + ( # ` ( B prefix ( N - L ) ) ) ) ) ) -> ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) = ( ( B prefix ( N - L ) ) ` ( k - ( # ` ( A substr <. M , L >. ) ) ) ) )
92 90 91 syl 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) = ( ( B prefix ( N - L ) ) ` ( k - ( # ` ( A substr <. M , L >. ) ) ) ) )
93 70 92 eqtr4d 
 |-  ( ( -. k e. ( 0 ..^ ( L - M ) ) /\ ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) )
94 65 93 pm2.61ian 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ` k ) )
95 4 47 94 eqfnfvd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
96 95 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )