Metamath Proof Explorer

Theorem swrdswrd

Description: A subword of a subword is a subword. (Contributed by Alexander van der Vekens, 4-Apr-2018)

Ref Expression
Assertion swrdswrd 
|- ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( W substr <. ( M + K ) , ( M + L ) >. ) ) )

Proof

Step Hyp Ref Expression
1 swrdcl 
 |-  ( W e. Word V -> ( W substr <. M , N >. ) e. Word V )
2 1 3ad2ant1 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( W substr <. M , N >. ) e. Word V )
3 2 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W substr <. M , N >. ) e. Word V )
4 elfz0ubfz0 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> K e. ( 0 ... L ) )
5 4 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> K e. ( 0 ... L ) )
6 elfzuz 
 |-  ( K e. ( 0 ... ( N - M ) ) -> K e. ( ZZ>= ` 0 ) )
7 6 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ K e. ( 0 ... ( N - M ) ) ) -> K e. ( ZZ>= ` 0 ) )
8 fzss1 
 |-  ( K e. ( ZZ>= ` 0 ) -> ( K ... ( N - M ) ) C_ ( 0 ... ( N - M ) ) )
9 7 8 syl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ K e. ( 0 ... ( N - M ) ) ) -> ( K ... ( N - M ) ) C_ ( 0 ... ( N - M ) ) )
10 9 sseld 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ K e. ( 0 ... ( N - M ) ) ) -> ( L e. ( K ... ( N - M ) ) -> L e. ( 0 ... ( N - M ) ) ) )
11 10 impr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> L e. ( 0 ... ( N - M ) ) )
12 3ancomb 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) <-> ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
13 12 biimpi 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
14 13 adantr 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
15 swrdlen 
 |-  ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
16 14 15 syl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( # ` ( W substr <. M , N >. ) ) = ( N - M ) )
17 16 oveq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( 0 ... ( # ` ( W substr <. M , N >. ) ) ) = ( 0 ... ( N - M ) ) )
18 11 17 eleqtrrd 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> L e. ( 0 ... ( # ` ( W substr <. M , N >. ) ) ) )
19 swrdval2 
 |-  ( ( ( W substr <. M , N >. ) e. Word V /\ K e. ( 0 ... L ) /\ L e. ( 0 ... ( # ` ( W substr <. M , N >. ) ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) )
20 3 5 18 19 syl3anc 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) )
21 fvex 
 |-  ( ( W substr <. M , N >. ) ` ( x + K ) ) e. _V
22 eqid 
 |-  ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) = ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) )
23 21 22 fnmpti 
 |-  ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) Fn ( 0 ..^ ( L - K ) )
24 23 a1i 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) Fn ( 0 ..^ ( L - K ) ) )
25 swrdswrdlem 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) )
26 swrdvalfn 
 |-  ( ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) -> ( W substr <. ( M + K ) , ( M + L ) >. ) Fn ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) )
27 25 26 syl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W substr <. ( M + K ) , ( M + L ) >. ) Fn ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) )
28 elfzelz 
 |-  ( M e. ( 0 ... N ) -> M e. ZZ )
29 elfzelz 
 |-  ( L e. ( K ... ( N - M ) ) -> L e. ZZ )
30 elfzelz 
 |-  ( K e. ( 0 ... ( N - M ) ) -> K e. ZZ )
31 zcn 
 |-  ( M e. ZZ -> M e. CC )
32 31 adantr 
 |-  ( ( M e. ZZ /\ ( L e. ZZ /\ K e. ZZ ) ) -> M e. CC )
33 zcn 
 |-  ( L e. ZZ -> L e. CC )
34 33 ad2antrl 
 |-  ( ( M e. ZZ /\ ( L e. ZZ /\ K e. ZZ ) ) -> L e. CC )
35 zcn 
 |-  ( K e. ZZ -> K e. CC )
36 35 ad2antll 
 |-  ( ( M e. ZZ /\ ( L e. ZZ /\ K e. ZZ ) ) -> K e. CC )
37 pnpcan 
 |-  ( ( M e. CC /\ L e. CC /\ K e. CC ) -> ( ( M + L ) - ( M + K ) ) = ( L - K ) )
38 37 eqcomd 
 |-  ( ( M e. CC /\ L e. CC /\ K e. CC ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) )
39 32 34 36 38 syl3anc 
 |-  ( ( M e. ZZ /\ ( L e. ZZ /\ K e. ZZ ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) )
40 39 expcom 
 |-  ( ( L e. ZZ /\ K e. ZZ ) -> ( M e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
41 29 30 40 syl2anr 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( M e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
42 28 41 syl5com 
 |-  ( M e. ( 0 ... N ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
43 42 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
44 43 imp 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) )
45 44 oveq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( 0 ..^ ( L - K ) ) = ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) )
46 45 fneq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( ( W substr <. ( M + K ) , ( M + L ) >. ) Fn ( 0 ..^ ( L - K ) ) <-> ( W substr <. ( M + K ) , ( M + L ) >. ) Fn ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) ) )
47 27 46 mpbird 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( W substr <. ( M + K ) , ( M + L ) >. ) Fn ( 0 ..^ ( L - K ) ) )
48 simpr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> y e. ( 0 ..^ ( L - K ) ) )
49 fvex 
 |-  ( W ` ( ( y + K ) + M ) ) e. _V
50 oveq1 
 |-  ( x = y -> ( x + K ) = ( y + K ) )
51 50 fvoveq1d 
 |-  ( x = y -> ( W ` ( ( x + K ) + M ) ) = ( W ` ( ( y + K ) + M ) ) )
52 eqid 
 |-  ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) = ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) )
53 51 52 fvmptg 
 |-  ( ( y e. ( 0 ..^ ( L - K ) ) /\ ( W ` ( ( y + K ) + M ) ) e. _V ) -> ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) ` y ) = ( W ` ( ( y + K ) + M ) ) )
54 48 49 53 sylancl 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) ` y ) = ( W ` ( ( y + K ) + M ) ) )
55 zcn 
 |-  ( y e. ZZ -> y e. CC )
56 55 31 35 3anim123i 
 |-  ( ( y e. ZZ /\ M e. ZZ /\ K e. ZZ ) -> ( y e. CC /\ M e. CC /\ K e. CC ) )
57 56 3expa 
 |-  ( ( ( y e. ZZ /\ M e. ZZ ) /\ K e. ZZ ) -> ( y e. CC /\ M e. CC /\ K e. CC ) )
58 add32r 
 |-  ( ( y e. CC /\ M e. CC /\ K e. CC ) -> ( y + ( M + K ) ) = ( ( y + K ) + M ) )
59 58 eqcomd 
 |-  ( ( y e. CC /\ M e. CC /\ K e. CC ) -> ( ( y + K ) + M ) = ( y + ( M + K ) ) )
60 57 59 syl 
 |-  ( ( ( y e. ZZ /\ M e. ZZ ) /\ K e. ZZ ) -> ( ( y + K ) + M ) = ( y + ( M + K ) ) )
61 60 exp31 
 |-  ( y e. ZZ -> ( M e. ZZ -> ( K e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
62 61 com13 
 |-  ( K e. ZZ -> ( M e. ZZ -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
63 30 62 syl 
 |-  ( K e. ( 0 ... ( N - M ) ) -> ( M e. ZZ -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
64 63 adantr 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( M e. ZZ -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
65 28 64 syl5com 
 |-  ( M e. ( 0 ... N ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
66 65 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) ) )
67 66 imp 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( y e. ZZ -> ( ( y + K ) + M ) = ( y + ( M + K ) ) ) )
68 elfzoelz 
 |-  ( y e. ( 0 ..^ ( L - K ) ) -> y e. ZZ )
69 67 68 impel 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( y + K ) + M ) = ( y + ( M + K ) ) )
70 69 fveq2d 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( W ` ( ( y + K ) + M ) ) = ( W ` ( y + ( M + K ) ) ) )
71 54 70 eqtrd 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) ` y ) = ( W ` ( y + ( M + K ) ) ) )
72 13 ad3antrrr 
 |-  ( ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) /\ x e. ( 0 ..^ ( L - K ) ) ) -> ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) )
73 elfz2nn0 
 |-  ( K e. ( 0 ... ( N - M ) ) <-> ( K e. NN0 /\ ( N - M ) e. NN0 /\ K <_ ( N - M ) ) )
74 elfz2 
 |-  ( L e. ( K ... ( N - M ) ) <-> ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) )
75 elfzo0 
 |-  ( x e. ( 0 ..^ ( L - K ) ) <-> ( x e. NN0 /\ ( L - K ) e. NN /\ x < ( L - K ) ) )
76 nn0re 
 |-  ( x e. NN0 -> x e. RR )
77 76 ad2antrl 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> x e. RR )
78 nn0re 
 |-  ( K e. NN0 -> K e. RR )
79 78 adantr 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> K e. RR )
80 zre 
 |-  ( L e. ZZ -> L e. RR )
81 80 ad2antll 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> L e. RR )
82 ltaddsub 
 |-  ( ( x e. RR /\ K e. RR /\ L e. RR ) -> ( ( x + K ) < L <-> x < ( L - K ) ) )
83 82 bicomd 
 |-  ( ( x e. RR /\ K e. RR /\ L e. RR ) -> ( x < ( L - K ) <-> ( x + K ) < L ) )
84 77 79 81 83 syl3anc 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( x < ( L - K ) <-> ( x + K ) < L ) )
85 nn0addcl 
 |-  ( ( x e. NN0 /\ K e. NN0 ) -> ( x + K ) e. NN0 )
86 85 ex 
 |-  ( x e. NN0 -> ( K e. NN0 -> ( x + K ) e. NN0 ) )
87 86 adantr 
 |-  ( ( x e. NN0 /\ L e. ZZ ) -> ( K e. NN0 -> ( x + K ) e. NN0 ) )
88 87 impcom 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( x + K ) e. NN0 )
89 88 ad3antrrr 
 |-  ( ( ( ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) /\ ( x + K ) < L ) /\ ( N - M ) e. NN0 ) /\ L <_ ( N - M ) ) -> ( x + K ) e. NN0 )
90 elnn0z 
 |-  ( ( x + K ) e. NN0 <-> ( ( x + K ) e. ZZ /\ 0 <_ ( x + K ) ) )
91 0red 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> 0 e. RR )
92 zre 
 |-  ( ( x + K ) e. ZZ -> ( x + K ) e. RR )
93 92 adantr 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( x + K ) e. RR )
94 80 adantl 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> L e. RR )
95 lelttr 
 |-  ( ( 0 e. RR /\ ( x + K ) e. RR /\ L e. RR ) -> ( ( 0 <_ ( x + K ) /\ ( x + K ) < L ) -> 0 < L ) )
96 91 93 94 95 syl3anc 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ ( x + K ) /\ ( x + K ) < L ) -> 0 < L ) )
97 0red 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> 0 e. RR )
98 80 adantr 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> L e. RR )
99 nn0re 
 |-  ( ( N - M ) e. NN0 -> ( N - M ) e. RR )
100 99 adantl 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> ( N - M ) e. RR )
101 ltletr 
 |-  ( ( 0 e. RR /\ L e. RR /\ ( N - M ) e. RR ) -> ( ( 0 < L /\ L <_ ( N - M ) ) -> 0 < ( N - M ) ) )
102 97 98 100 101 syl3anc 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> ( ( 0 < L /\ L <_ ( N - M ) ) -> 0 < ( N - M ) ) )
103 elnnnn0b 
 |-  ( ( N - M ) e. NN <-> ( ( N - M ) e. NN0 /\ 0 < ( N - M ) ) )
104 103 simplbi2 
 |-  ( ( N - M ) e. NN0 -> ( 0 < ( N - M ) -> ( N - M ) e. NN ) )
105 104 adantl 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> ( 0 < ( N - M ) -> ( N - M ) e. NN ) )
106 102 105 syld 
 |-  ( ( L e. ZZ /\ ( N - M ) e. NN0 ) -> ( ( 0 < L /\ L <_ ( N - M ) ) -> ( N - M ) e. NN ) )
107 106 exp4b 
 |-  ( L e. ZZ -> ( ( N - M ) e. NN0 -> ( 0 < L -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) )
108 107 com23 
 |-  ( L e. ZZ -> ( 0 < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) )
109 108 adantl 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( 0 < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) )
110 96 109 syld 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( ( 0 <_ ( x + K ) /\ ( x + K ) < L ) -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) )
111 110 expd 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( 0 <_ ( x + K ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) )
112 111 a1d 
 |-  ( ( ( x + K ) e. ZZ /\ L e. ZZ ) -> ( ( x e. NN0 /\ K e. NN0 ) -> ( 0 <_ ( x + K ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) ) )
113 112 ex 
 |-  ( ( x + K ) e. ZZ -> ( L e. ZZ -> ( ( x e. NN0 /\ K e. NN0 ) -> ( 0 <_ ( x + K ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) ) ) )
114 113 com24 
 |-  ( ( x + K ) e. ZZ -> ( 0 <_ ( x + K ) -> ( ( x e. NN0 /\ K e. NN0 ) -> ( L e. ZZ -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) ) ) )
115 114 imp 
 |-  ( ( ( x + K ) e. ZZ /\ 0 <_ ( x + K ) ) -> ( ( x e. NN0 /\ K e. NN0 ) -> ( L e. ZZ -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) ) )
116 90 115 sylbi 
 |-  ( ( x + K ) e. NN0 -> ( ( x e. NN0 /\ K e. NN0 ) -> ( L e. ZZ -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) ) )
117 85 116 mpcom 
 |-  ( ( x e. NN0 /\ K e. NN0 ) -> ( L e. ZZ -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) )
118 117 impancom 
 |-  ( ( x e. NN0 /\ L e. ZZ ) -> ( K e. NN0 -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) ) )
119 118 impcom 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( N - M ) e. NN ) ) ) )
120 119 imp41 
 |-  ( ( ( ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) /\ ( x + K ) < L ) /\ ( N - M ) e. NN0 ) /\ L <_ ( N - M ) ) -> ( N - M ) e. NN )
121 nn0readdcl 
 |-  ( ( x e. NN0 /\ K e. NN0 ) -> ( x + K ) e. RR )
122 121 ex 
 |-  ( x e. NN0 -> ( K e. NN0 -> ( x + K ) e. RR ) )
123 122 adantr 
 |-  ( ( x e. NN0 /\ L e. ZZ ) -> ( K e. NN0 -> ( x + K ) e. RR ) )
124 123 impcom 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( x + K ) e. RR )
125 ltletr 
 |-  ( ( ( x + K ) e. RR /\ L e. RR /\ ( N - M ) e. RR ) -> ( ( ( x + K ) < L /\ L <_ ( N - M ) ) -> ( x + K ) < ( N - M ) ) )
126 124 81 99 125 syl2an3an 
 |-  ( ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) /\ ( N - M ) e. NN0 ) -> ( ( ( x + K ) < L /\ L <_ ( N - M ) ) -> ( x + K ) < ( N - M ) ) )
127 126 exp4b 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( ( N - M ) e. NN0 -> ( ( x + K ) < L -> ( L <_ ( N - M ) -> ( x + K ) < ( N - M ) ) ) ) )
128 127 com23 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( x + K ) < ( N - M ) ) ) ) )
129 128 imp41 
 |-  ( ( ( ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) /\ ( x + K ) < L ) /\ ( N - M ) e. NN0 ) /\ L <_ ( N - M ) ) -> ( x + K ) < ( N - M ) )
130 elfzo0 
 |-  ( ( x + K ) e. ( 0 ..^ ( N - M ) ) <-> ( ( x + K ) e. NN0 /\ ( N - M ) e. NN /\ ( x + K ) < ( N - M ) ) )
131 89 120 129 130 syl3anbrc 
 |-  ( ( ( ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) /\ ( x + K ) < L ) /\ ( N - M ) e. NN0 ) /\ L <_ ( N - M ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) )
132 131 exp41 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( ( x + K ) < L -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
133 84 132 sylbid 
 |-  ( ( K e. NN0 /\ ( x e. NN0 /\ L e. ZZ ) ) -> ( x < ( L - K ) -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
134 133 ex 
 |-  ( K e. NN0 -> ( ( x e. NN0 /\ L e. ZZ ) -> ( x < ( L - K ) -> ( ( N - M ) e. NN0 -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) ) )
135 134 com24 
 |-  ( K e. NN0 -> ( ( N - M ) e. NN0 -> ( x < ( L - K ) -> ( ( x e. NN0 /\ L e. ZZ ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) ) )
136 135 imp 
 |-  ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x < ( L - K ) -> ( ( x e. NN0 /\ L e. ZZ ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
137 136 com13 
 |-  ( ( x e. NN0 /\ L e. ZZ ) -> ( x < ( L - K ) -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
138 137 impancom 
 |-  ( ( x e. NN0 /\ x < ( L - K ) ) -> ( L e. ZZ -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
139 138 3adant2 
 |-  ( ( x e. NN0 /\ ( L - K ) e. NN /\ x < ( L - K ) ) -> ( L e. ZZ -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
140 75 139 sylbi 
 |-  ( x e. ( 0 ..^ ( L - K ) ) -> ( L e. ZZ -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( L <_ ( N - M ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
141 140 com14 
 |-  ( L <_ ( N - M ) -> ( L e. ZZ -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
142 141 adantl 
 |-  ( ( K <_ L /\ L <_ ( N - M ) ) -> ( L e. ZZ -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
143 142 com12 
 |-  ( L e. ZZ -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
144 143 3ad2ant3 
 |-  ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) -> ( ( K <_ L /\ L <_ ( N - M ) ) -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) ) )
145 144 imp 
 |-  ( ( ( K e. ZZ /\ ( N - M ) e. ZZ /\ L e. ZZ ) /\ ( K <_ L /\ L <_ ( N - M ) ) ) -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) )
146 74 145 sylbi 
 |-  ( L e. ( K ... ( N - M ) ) -> ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) )
147 146 com12 
 |-  ( ( K e. NN0 /\ ( N - M ) e. NN0 ) -> ( L e. ( K ... ( N - M ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) )
148 147 3adant3 
 |-  ( ( K e. NN0 /\ ( N - M ) e. NN0 /\ K <_ ( N - M ) ) -> ( L e. ( K ... ( N - M ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) )
149 73 148 sylbi 
 |-  ( K e. ( 0 ... ( N - M ) ) -> ( L e. ( K ... ( N - M ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) ) )
150 149 imp 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) )
151 150 adantl 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) )
152 151 adantr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) ) )
153 152 imp 
 |-  ( ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) /\ x e. ( 0 ..^ ( L - K ) ) ) -> ( x + K ) e. ( 0 ..^ ( N - M ) ) )
154 swrdfv 
 |-  ( ( ( W e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... ( # ` W ) ) ) /\ ( x + K ) e. ( 0 ..^ ( N - M ) ) ) -> ( ( W substr <. M , N >. ) ` ( x + K ) ) = ( W ` ( ( x + K ) + M ) ) )
155 72 153 154 syl2anc 
 |-  ( ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) /\ x e. ( 0 ..^ ( L - K ) ) ) -> ( ( W substr <. M , N >. ) ` ( x + K ) ) = ( W ` ( ( x + K ) + M ) ) )
156 155 mpteq2dva 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) = ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) )
157 156 fveq1d 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) ` y ) = ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( W ` ( ( x + K ) + M ) ) ) ` y ) )
158 25 adantr 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) )
159 31 33 35 3anim123i 
 |-  ( ( M e. ZZ /\ L e. ZZ /\ K e. ZZ ) -> ( M e. CC /\ L e. CC /\ K e. CC ) )
160 159 3expa 
 |-  ( ( ( M e. ZZ /\ L e. ZZ ) /\ K e. ZZ ) -> ( M e. CC /\ L e. CC /\ K e. CC ) )
161 160 38 syl 
 |-  ( ( ( M e. ZZ /\ L e. ZZ ) /\ K e. ZZ ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) )
162 161 exp31 
 |-  ( M e. ZZ -> ( L e. ZZ -> ( K e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) ) )
163 162 com3l 
 |-  ( L e. ZZ -> ( K e. ZZ -> ( M e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) ) )
164 29 163 syl 
 |-  ( L e. ( K ... ( N - M ) ) -> ( K e. ZZ -> ( M e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) ) )
165 30 164 mpan9 
 |-  ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( M e. ZZ -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
166 28 165 syl5com 
 |-  ( M e. ( 0 ... N ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
167 166 3ad2ant3 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) ) )
168 167 imp 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( L - K ) = ( ( M + L ) - ( M + K ) ) )
169 168 oveq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( 0 ..^ ( L - K ) ) = ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) )
170 169 eleq2d 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( y e. ( 0 ..^ ( L - K ) ) <-> y e. ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) ) )
171 170 biimpa 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> y e. ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) )
172 swrdfv 
 |-  ( ( ( W e. Word V /\ ( M + K ) e. ( 0 ... ( M + L ) ) /\ ( M + L ) e. ( 0 ... ( # ` W ) ) ) /\ y e. ( 0 ..^ ( ( M + L ) - ( M + K ) ) ) ) -> ( ( W substr <. ( M + K ) , ( M + L ) >. ) ` y ) = ( W ` ( y + ( M + K ) ) ) )
173 158 171 172 syl2anc 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( W substr <. ( M + K ) , ( M + L ) >. ) ` y ) = ( W ` ( y + ( M + K ) ) ) )
174 71 157 173 3eqtr4d 
 |-  ( ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) /\ y e. ( 0 ..^ ( L - K ) ) ) -> ( ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) ` y ) = ( ( W substr <. ( M + K ) , ( M + L ) >. ) ` y ) )
175 24 47 174 eqfnfvd 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( x e. ( 0 ..^ ( L - K ) ) |-> ( ( W substr <. M , N >. ) ` ( x + K ) ) ) = ( W substr <. ( M + K ) , ( M + L ) >. ) )
176 20 175 eqtrd 
 |-  ( ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) /\ ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( W substr <. ( M + K ) , ( M + L ) >. ) )
177 176 ex 
 |-  ( ( W e. Word V /\ N e. ( 0 ... ( # ` W ) ) /\ M e. ( 0 ... N ) ) -> ( ( K e. ( 0 ... ( N - M ) ) /\ L e. ( K ... ( N - M ) ) ) -> ( ( W substr <. M , N >. ) substr <. K , L >. ) = ( W substr <. ( M + K ) , ( M + L ) >. ) ) )