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

Metamath Proof Explorer

Theorem pfxccatin12lem2

Description: Lemma 2 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 9-May-2020)

Ref Expression
Hypothesis swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion pfxccatin12lem2 ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 1 pfxccatin12lem2c ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
3 simprl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
4 swrdfv ⊢ ( ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) )
5 2 3 4 syl2an2r ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) )
6 elfzoelz ⊢ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → 𝐾 ∈ ℤ )
7 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
8 nn0cn ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℂ )
9 nn0cn ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℂ )
10 8 9 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) )
11 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
12 subcl ⊢ ( ( 𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
13 12 ancoms ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
14 13 anim1ci ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( 𝐾 ∈ ℂ ∧ ( 𝐿 − 𝑀 ) ∈ ℂ ) )
15 subcl ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 𝐿 − 𝑀 ) ∈ ℂ ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ℂ )
16 14 15 syl ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ℂ )
17 16 addridd ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) = ( 𝐾 − ( 𝐿 − 𝑀 ) ) )
18 simpr ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → 𝐾 ∈ ℂ )
19 simplr ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → 𝐿 ∈ ℂ )
20 simpll ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → 𝑀 ∈ ℂ )
21 18 19 20 subsub3d ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) = ( ( 𝐾 + 𝑀 ) − 𝐿 ) )
22 17 21 eqtr2d ⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( ( 𝐾 + 𝑀 ) − 𝐿 ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) )
23 10 11 22 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 + 𝑀 ) − 𝐿 ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) )
24 oveq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 + 𝑀 ) − 𝐿 ) )
25 24 eqcoms ⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 + 𝑀 ) − 𝐿 ) )
26 25 eqeq1d ⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ↔ ( ( 𝐾 + 𝑀 ) − 𝐿 ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
27 23 26 imbitrrid ⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
28 1 27 ax-mp ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) )
29 28 ex ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
30 29 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
31 7 30 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
32 31 ad2antrl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝐾 ∈ ℤ → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
33 6 32 syl5com ⊢ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
34 33 adantr ⊢ ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
35 34 impcom ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) )
36 35 fveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐵 ‘ ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) ) = ( 𝐵 ‘ ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
37 simpll ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
38 pfxccatin12lem2a ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
39 38 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
40 39 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
41 id ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ♯ ‘ 𝐴 ) = 𝐿 )
42 oveq1 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) = ( 𝐿 + ( ♯ ‘ 𝐵 ) ) )
43 41 42 oveq12d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) = ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
44 43 eleq2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
45 44 eqcoms ⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
46 1 45 ax-mp ⊢ ( ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ↔ ( 𝐾 + 𝑀 ) ∈ ( 𝐿 ..^ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
47 40 46 sylibr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) )
48 df-3an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) ↔ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
49 37 47 48 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) )
50 ccatval2 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( ( ♯ ‘ 𝐴 ) ..^ ( ( ♯ ‘ 𝐴 ) + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) = ( 𝐵 ‘ ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) ) )
51 49 50 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) = ( 𝐵 ‘ ( ( 𝐾 + 𝑀 ) − ( ♯ ‘ 𝐴 ) ) ) )
52 simplr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐵 ∈ Word 𝑉 )
53 52 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐵 ∈ Word 𝑉 )
54 lencl ⊢ ( 𝐵 ∈ Word 𝑉 → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
55 elfzel2 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℤ )
56 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
57 56 ancoms ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
58 57 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
59 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
60 zre ⊢ ( 𝐿 ∈ ℤ → 𝐿 ∈ ℝ )
61 subge0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 0 ≤ ( 𝑁 − 𝐿 ) ↔ 𝐿 ≤ 𝑁 ) )
62 59 60 61 syl2anr ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ≤ ( 𝑁 − 𝐿 ) ↔ 𝐿 ≤ 𝑁 ) )
63 62 biimprd ⊢ ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ≤ 𝑁 → 0 ≤ ( 𝑁 − 𝐿 ) ) )
64 63 imp ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐿 ≤ 𝑁 ) → 0 ≤ ( 𝑁 − 𝐿 ) )
65 elnn0z ⊢ ( ( 𝑁 − 𝐿 ) ∈ ℕ0 ↔ ( ( 𝑁 − 𝐿 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 𝐿 ) ) )
66 58 64 65 sylanbrc ⊢ ( ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 )
67 66 expcom ⊢ ( 𝐿 ≤ 𝑁 → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
68 67 adantr ⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
69 68 expcomd ⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝑁 ∈ ℤ → ( 𝐿 ∈ ℤ → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) ) )
70 69 com12 ⊢ ( 𝑁 ∈ ℤ → ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 ∈ ℤ → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) ) )
71 70 3ad2ant3 ⊢ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝐿 ∈ ℤ → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) ) )
72 71 imp ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝐿 ∈ ℤ → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
73 72 com12 ⊢ ( 𝐿 ∈ ℤ → ( ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
74 73 adantr ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
75 74 imp ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 )
76 simplr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
77 59 3ad2ant3 ⊢ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℝ )
78 77 adantl ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝑁 ∈ ℝ )
79 60 adantr ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → 𝐿 ∈ ℝ )
80 79 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → 𝐿 ∈ ℝ )
81 nn0re ⊢ ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( ♯ ‘ 𝐵 ) ∈ ℝ )
82 81 adantl ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
83 82 adantr ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ♯ ‘ 𝐵 ) ∈ ℝ )
84 lesubadd2 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) → ( ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) )
85 84 biimprd ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ ( ♯ ‘ 𝐵 ) ∈ ℝ ) → ( 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) )
86 78 80 83 85 syl3anc ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) )
87 86 ex ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
88 87 com13 ⊢ ( 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
89 88 adantl ⊢ ( ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
90 89 impcom ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) )
91 90 impcom ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) )
92 75 76 91 3jca ⊢ ( ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) ∧ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝑁 − 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) )
93 92 ex ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝑁 − 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) ) )
94 elfz2 ⊢ ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ↔ ( ( 𝐿 ∈ ℤ ∧ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐿 ≤ 𝑁 ∧ 𝑁 ≤ ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) )
95 elfz2nn0 ⊢ ( ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ↔ ( ( 𝑁 − 𝐿 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ∧ ( 𝑁 − 𝐿 ) ≤ ( ♯ ‘ 𝐵 ) ) )
96 93 94 95 3imtr4g ⊢ ( ( 𝐿 ∈ ℤ ∧ ( ♯ ‘ 𝐵 ) ∈ ℕ0 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) )
97 96 ex ⊢ ( 𝐿 ∈ ℤ → ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) ) )
98 97 com23 ⊢ ( 𝐿 ∈ ℤ → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) ) )
99 55 98 syl ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) ) )
100 99 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( ♯ ‘ 𝐵 ) ∈ ℕ0 → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) )
101 54 100 syl5com ⊢ ( 𝐵 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) )
102 101 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ) )
103 102 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
104 103 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) )
105 pfxccatin12lem1 ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )
106 105 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) )
107 106 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) )
108 pfxfv ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑁 − 𝐿 ) ∈ ( 0 ... ( ♯ ‘ 𝐵 ) ) ∧ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ( 0 ..^ ( 𝑁 − 𝐿 ) ) ) → ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) = ( 𝐵 ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) )
109 53 104 107 108 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) = ( 𝐵 ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) )
110 6 zcnd ⊢ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) → 𝐾 ∈ ℂ )
111 110 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ℂ )
112 55 zcnd ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → 𝐿 ∈ ℂ )
113 112 ad2antrl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐿 ∈ ℂ )
114 113 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐿 ∈ ℂ )
115 elfzelz ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → 𝑀 ∈ ℤ )
116 115 zcnd ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → 𝑀 ∈ ℂ )
117 116 ad2antrl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝑀 ∈ ℂ )
118 117 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝑀 ∈ ℂ )
119 114 118 subcld ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐿 − 𝑀 ) ∈ ℂ )
120 111 119 subcld ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) ∈ ℂ )
121 120 addridd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) = ( 𝐾 − ( 𝐿 − 𝑀 ) ) )
122 121 eqcomd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) = ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) )
123 122 fveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐵 ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) = ( 𝐵 ‘ ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
124 109 123 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) = ( 𝐵 ‘ ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 0 ) ) )
125 36 51 124 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) )
126 simpll ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ Word 𝑉 )
127 simprl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝑀 ∈ ( 0 ... 𝐿 ) )
128 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
129 elnn0uz ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
130 eluzfz2 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) → ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
131 129 130 sylbi ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ 𝐴 ) ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
132 1 131 eqeltrid ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
133 128 132 syl ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
134 133 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
135 134 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
136 126 127 135 3jca ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
137 136 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) )
138 swrdlen ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝑀 ) )
139 137 138 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) = ( 𝐿 − 𝑀 ) )
140 139 eqcomd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐿 − 𝑀 ) = ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) )
141 140 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 − ( 𝐿 − 𝑀 ) ) = ( 𝐾 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) )
142 141 fveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( 𝐿 − 𝑀 ) ) ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
143 5 125 142 3eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) )
144 143 ex ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ ¬ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ‘ ( 𝐾 − ( ♯ ‘ ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) ) )