Metamath Proof Explorer

Theorem swrdccatin2

Description: The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018) (Revised by Alexander van der Vekens, 27-May-2018)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l 
 |-  L = ( # ` A )
2 oveq1 
 |-  ( L = ( # ` A ) -> ( L ... N ) = ( ( # ` A ) ... N ) )
3 2 eleq2d 
 |-  ( L = ( # ` A ) -> ( M e. ( L ... N ) <-> M e. ( ( # ` A ) ... N ) ) )
4 id 
 |-  ( L = ( # ` A ) -> L = ( # ` A ) )
5 oveq1 
 |-  ( L = ( # ` A ) -> ( L + ( # ` B ) ) = ( ( # ` A ) + ( # ` B ) ) )
6 4 5 oveq12d 
 |-  ( L = ( # ` A ) -> ( L ... ( L + ( # ` B ) ) ) = ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) )
7 6 eleq2d 
 |-  ( L = ( # ` A ) -> ( N e. ( L ... ( L + ( # ` B ) ) ) <-> N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) )
8 3 7 anbi12d 
 |-  ( L = ( # ` A ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) <-> ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
9 1 8 ax-mp 
 |-  ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) <-> ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) )
10 lencl 
 |-  ( A e. Word V -> ( # ` A ) e. NN0 )
11 elnn0uz 
 |-  ( ( # ` A ) e. NN0 <-> ( # ` A ) e. ( ZZ>= ` 0 ) )
12 fzss1 
 |-  ( ( # ` A ) e. ( ZZ>= ` 0 ) -> ( ( # ` A ) ... N ) C_ ( 0 ... N ) )
13 11 12 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( ( # ` A ) ... N ) C_ ( 0 ... N ) )
14 13 sseld 
 |-  ( ( # ` A ) e. NN0 -> ( M e. ( ( # ` A ) ... N ) -> M e. ( 0 ... N ) ) )
15 fzss1 
 |-  ( ( # ` A ) e. ( ZZ>= ` 0 ) -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) C_ ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
16 11 15 sylbi 
 |-  ( ( # ` A ) e. NN0 -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) C_ ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
17 16 sseld 
 |-  ( ( # ` A ) e. NN0 -> ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
18 14 17 anim12d 
 |-  ( ( # ` A ) e. NN0 -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
19 10 18 syl 
 |-  ( A e. Word V -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
20 19 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( ( # ` A ) ... N ) /\ N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
21 9 20 biimtrid 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) )
22 21 imp 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
23 swrdccatfn 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
24 22 23 syldan 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) )
25 fzmmmeqm 
 |-  ( M e. ( L ... N ) -> ( ( N - L ) - ( M - L ) ) = ( N - M ) )
26 25 oveq2d 
 |-  ( M e. ( L ... N ) -> ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) = ( 0 ..^ ( N - M ) ) )
27 26 fneq2d 
 |-  ( M e. ( L ... N ) -> ( ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) <-> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) ) )
28 27 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) <-> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( N - M ) ) ) )
29 24 28 mpbird 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) Fn ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) )
30 simplr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> B e. Word V )
31 elfzmlbm 
 |-  ( M e. ( L ... N ) -> ( M - L ) e. ( 0 ... ( N - L ) ) )
32 31 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( M - L ) e. ( 0 ... ( N - L ) ) )
33 lencl 
 |-  ( B e. Word V -> ( # ` B ) e. NN0 )
34 33 nn0zd 
 |-  ( B e. Word V -> ( # ` B ) e. ZZ )
35 34 adantl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` B ) e. ZZ )
36 elfzmlbp 
 |-  ( ( ( # ` B ) e. ZZ /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
37 35 36 sylan 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
38 37 adantrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
39 swrdvalfn 
 |-  ( ( B e. Word V /\ ( M - L ) e. ( 0 ... ( N - L ) ) /\ ( N - L ) e. ( 0 ... ( # ` B ) ) ) -> ( B substr <. ( M - L ) , ( N - L ) >. ) Fn ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) )
40 30 32 38 39 syl3anc 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( B substr <. ( M - L ) , ( N - L ) >. ) Fn ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) )
41 simpll 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( A e. Word V /\ B e. Word V ) )
42 elfzelz 
 |-  ( M e. ( L ... N ) -> M e. ZZ )
43 zaddcl 
 |-  ( ( k e. ZZ /\ M e. ZZ ) -> ( k + M ) e. ZZ )
44 43 expcom 
 |-  ( M e. ZZ -> ( k e. ZZ -> ( k + M ) e. ZZ ) )
45 42 44 syl 
 |-  ( M e. ( L ... N ) -> ( k e. ZZ -> ( k + M ) e. ZZ ) )
46 45 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( k e. ZZ -> ( k + M ) e. ZZ ) )
47 elfzoelz 
 |-  ( k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) -> k e. ZZ )
48 46 47 impel 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( k + M ) e. ZZ )
49 df-3an 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( k + M ) e. ZZ ) <-> ( ( A e. Word V /\ B e. Word V ) /\ ( k + M ) e. ZZ ) )
50 41 48 49 sylanbrc 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( A e. Word V /\ B e. Word V /\ ( k + M ) e. ZZ ) )
51 ccatsymb 
 |-  ( ( A e. Word V /\ B e. Word V /\ ( k + M ) e. ZZ ) -> ( ( A ++ B ) ` ( k + M ) ) = if ( ( k + M ) < ( # ` A ) , ( A ` ( k + M ) ) , ( B ` ( ( k + M ) - ( # ` A ) ) ) ) )
52 50 51 syl 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( A ++ B ) ` ( k + M ) ) = if ( ( k + M ) < ( # ` A ) , ( A ` ( k + M ) ) , ( B ` ( ( k + M ) - ( # ` A ) ) ) ) )
53 elfz2 
 |-  ( M e. ( L ... N ) <-> ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) )
54 zre 
 |-  ( L e. ZZ -> L e. RR )
55 zre 
 |-  ( M e. ZZ -> M e. RR )
56 54 55 anim12i 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( L e. RR /\ M e. RR ) )
57 elnn0z 
 |-  ( k e. NN0 <-> ( k e. ZZ /\ 0 <_ k ) )
58 zre 
 |-  ( k e. ZZ -> k e. RR )
59 0re 
 |-  0 e. RR
60 59 jctl 
 |-  ( L e. RR -> ( 0 e. RR /\ L e. RR ) )
61 60 ad2antrl 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( 0 e. RR /\ L e. RR ) )
62 id 
 |-  ( ( k e. RR /\ M e. RR ) -> ( k e. RR /\ M e. RR ) )
63 62 adantrl 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( k e. RR /\ M e. RR ) )
64 le2add 
 |-  ( ( ( 0 e. RR /\ L e. RR ) /\ ( k e. RR /\ M e. RR ) ) -> ( ( 0 <_ k /\ L <_ M ) -> ( 0 + L ) <_ ( k + M ) ) )
65 61 63 64 syl2anc 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( ( 0 <_ k /\ L <_ M ) -> ( 0 + L ) <_ ( k + M ) ) )
66 recn 
 |-  ( L e. RR -> L e. CC )
67 66 addlidd 
 |-  ( L e. RR -> ( 0 + L ) = L )
68 67 ad2antrl 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( 0 + L ) = L )
69 68 breq1d 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( ( 0 + L ) <_ ( k + M ) <-> L <_ ( k + M ) ) )
70 65 69 sylibd 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( ( 0 <_ k /\ L <_ M ) -> L <_ ( k + M ) ) )
71 simprl 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> L e. RR )
72 readdcl 
 |-  ( ( k e. RR /\ M e. RR ) -> ( k + M ) e. RR )
73 72 adantrl 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( k + M ) e. RR )
74 71 73 lenltd 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( L <_ ( k + M ) <-> -. ( k + M ) < L ) )
75 70 74 sylibd 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( ( 0 <_ k /\ L <_ M ) -> -. ( k + M ) < L ) )
76 75 expd 
 |-  ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( 0 <_ k -> ( L <_ M -> -. ( k + M ) < L ) ) )
77 76 com12 
 |-  ( 0 <_ k -> ( ( k e. RR /\ ( L e. RR /\ M e. RR ) ) -> ( L <_ M -> -. ( k + M ) < L ) ) )
78 77 expd 
 |-  ( 0 <_ k -> ( k e. RR -> ( ( L e. RR /\ M e. RR ) -> ( L <_ M -> -. ( k + M ) < L ) ) ) )
79 58 78 mpan9 
 |-  ( ( k e. ZZ /\ 0 <_ k ) -> ( ( L e. RR /\ M e. RR ) -> ( L <_ M -> -. ( k + M ) < L ) ) )
80 57 79 sylbi 
 |-  ( k e. NN0 -> ( ( L e. RR /\ M e. RR ) -> ( L <_ M -> -. ( k + M ) < L ) ) )
81 56 80 mpan9 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. NN0 ) -> ( L <_ M -> -. ( k + M ) < L ) )
82 1 breq2i 
 |-  ( ( k + M ) < L <-> ( k + M ) < ( # ` A ) )
83 82 notbii 
 |-  ( -. ( k + M ) < L <-> -. ( k + M ) < ( # ` A ) )
84 81 83 imbitrdi 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. NN0 ) -> ( L <_ M -> -. ( k + M ) < ( # ` A ) ) )
85 84 ex 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( k e. NN0 -> ( L <_ M -> -. ( k + M ) < ( # ` A ) ) ) )
86 85 com23 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( L <_ M -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) ) )
87 86 3adant2 
 |-  ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( L <_ M -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) ) )
88 87 imp 
 |-  ( ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ L <_ M ) -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) )
89 88 adantrr 
 |-  ( ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) )
90 53 89 sylbi 
 |-  ( M e. ( L ... N ) -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) )
91 90 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( k e. NN0 -> -. ( k + M ) < ( # ` A ) ) )
92 elfzonn0 
 |-  ( k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) -> k e. NN0 )
93 91 92 impel 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> -. ( k + M ) < ( # ` A ) )
94 93 iffalsed 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> if ( ( k + M ) < ( # ` A ) , ( A ` ( k + M ) ) , ( B ` ( ( k + M ) - ( # ` A ) ) ) ) = ( B ` ( ( k + M ) - ( # ` A ) ) ) )
95 zcn 
 |-  ( k e. ZZ -> k e. CC )
96 95 adantl 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> k e. CC )
97 zcn 
 |-  ( M e. ZZ -> M e. CC )
98 97 ad2antlr 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> M e. CC )
99 zcn 
 |-  ( L e. ZZ -> L e. CC )
100 99 ad2antrr 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> L e. CC )
101 96 98 100 addsubassd 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> ( ( k + M ) - L ) = ( k + ( M - L ) ) )
102 oveq2 
 |-  ( L = ( # ` A ) -> ( ( k + M ) - L ) = ( ( k + M ) - ( # ` A ) ) )
103 102 eqeq1d 
 |-  ( L = ( # ` A ) -> ( ( ( k + M ) - L ) = ( k + ( M - L ) ) <-> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
104 101 103 imbitrid 
 |-  ( L = ( # ` A ) -> ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
105 1 104 ax-mp 
 |-  ( ( ( L e. ZZ /\ M e. ZZ ) /\ k e. ZZ ) -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) )
106 105 ex 
 |-  ( ( L e. ZZ /\ M e. ZZ ) -> ( k e. ZZ -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
107 106 3adant2 
 |-  ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) -> ( k e. ZZ -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
108 107 adantr 
 |-  ( ( ( L e. ZZ /\ N e. ZZ /\ M e. ZZ ) /\ ( L <_ M /\ M <_ N ) ) -> ( k e. ZZ -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
109 53 108 sylbi 
 |-  ( M e. ( L ... N ) -> ( k e. ZZ -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
110 109 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( k e. ZZ -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) ) )
111 110 47 impel 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( k + M ) - ( # ` A ) ) = ( k + ( M - L ) ) )
112 111 fveq2d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( B ` ( ( k + M ) - ( # ` A ) ) ) = ( B ` ( k + ( M - L ) ) ) )
113 52 94 112 3eqtrd 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( A ++ B ) ` ( k + M ) ) = ( B ` ( k + ( M - L ) ) ) )
114 ccatcl 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) e. Word V )
115 114 adantr 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( A ++ B ) e. Word V )
116 11 biimpi 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. ( ZZ>= ` 0 ) )
117 1 116 eqeltrid 
 |-  ( ( # ` A ) e. NN0 -> L e. ( ZZ>= ` 0 ) )
118 fzss1 
 |-  ( L e. ( ZZ>= ` 0 ) -> ( L ... N ) C_ ( 0 ... N ) )
119 10 117 118 3syl 
 |-  ( A e. Word V -> ( L ... N ) C_ ( 0 ... N ) )
120 119 sselda 
 |-  ( ( A e. Word V /\ M e. ( L ... N ) ) -> M e. ( 0 ... N ) )
121 120 ad2ant2r 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> M e. ( 0 ... N ) )
122 1 7 ax-mp 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) <-> N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) )
123 10 116 15 3syl 
 |-  ( A e. Word V -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) C_ ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
124 123 adantr 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) C_ ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
125 124 sseld 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
126 125 impcom 
 |-  ( ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) /\ ( A e. Word V /\ B e. Word V ) ) -> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
127 ccatlen 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( # ` ( A ++ B ) ) = ( ( # ` A ) + ( # ` B ) ) )
128 127 oveq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( 0 ... ( # ` ( A ++ B ) ) ) = ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) )
129 128 eleq2d 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
130 129 adantl 
 |-  ( ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) /\ ( A e. Word V /\ B e. Word V ) ) -> ( N e. ( 0 ... ( # ` ( A ++ B ) ) ) <-> N e. ( 0 ... ( ( # ` A ) + ( # ` B ) ) ) ) )
131 126 130 mpbird 
 |-  ( ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) /\ ( A e. Word V /\ B e. Word V ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
132 131 ex 
 |-  ( N e. ( ( # ` A ) ... ( ( # ` A ) + ( # ` B ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
133 122 132 sylbi 
 |-  ( N e. ( L ... ( L + ( # ` B ) ) ) -> ( ( A e. Word V /\ B e. Word V ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
134 133 impcom 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
135 134 adantrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) )
136 115 121 135 3jca 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
137 26 eleq2d 
 |-  ( M e. ( L ... N ) -> ( k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) <-> k e. ( 0 ..^ ( N - M ) ) ) )
138 137 ad2antrl 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) <-> k e. ( 0 ..^ ( N - M ) ) ) )
139 138 biimpa 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> k e. ( 0 ..^ ( N - M ) ) )
140 swrdfv 
 |-  ( ( ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) /\ k e. ( 0 ..^ ( N - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A ++ B ) ` ( k + M ) ) )
141 136 139 140 syl2an2r 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( A ++ B ) ` ( k + M ) ) )
142 34 36 sylan 
 |-  ( ( B e. Word V /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
143 142 ad2ant2l 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( N - L ) e. ( 0 ... ( # ` B ) ) )
144 30 32 143 3jca 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( B e. Word V /\ ( M - L ) e. ( 0 ... ( N - L ) ) /\ ( N - L ) e. ( 0 ... ( # ` B ) ) ) )
145 swrdfv 
 |-  ( ( ( B e. Word V /\ ( M - L ) e. ( 0 ... ( N - L ) ) /\ ( N - L ) e. ( 0 ... ( # ` B ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( B substr <. ( M - L ) , ( N - L ) >. ) ` k ) = ( B ` ( k + ( M - L ) ) ) )
146 144 145 sylan 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( B substr <. ( M - L ) , ( N - L ) >. ) ` k ) = ( B ` ( k + ( M - L ) ) ) )
147 113 141 146 3eqtr4d 
 |-  ( ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) /\ k e. ( 0 ..^ ( ( N - L ) - ( M - L ) ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` k ) = ( ( B substr <. ( M - L ) , ( N - L ) >. ) ` k ) )
148 29 40 147 eqfnfvd 
 |-  ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
149 148 ex 
 |-  ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + ( # ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )