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

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 ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝐾 ∈ ( 0 ... ( 𝑁 − 𝑀 ) ) ∧ 𝐿 ∈ ( 𝐾 ... ( 𝑁 − 𝑀 ) ) ) → ( ( 𝑊 substr ⟨ 𝑀 , 𝑁 ⟩ ) substr ⟨ 𝐾 , 𝐿 ⟩ ) = ( 𝑊 substr ⟨ ( 𝑀 + 𝐾 ) , ( 𝑀 + 𝐿 ) ⟩ ) ) )

Proof

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