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

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 ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion swrdccatin2 ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 𝐿 ... 𝑁 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )

Proof

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