Metamath Proof Explorer

Theorem swrdccat

Description: The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018)

Ref Expression
Hypothesis swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
Assertion swrdccat ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) ) )

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 1 pfxccat3 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )
3 2 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
4 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
5 4 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
6 1 eqcomi ⊢ ( ♯ ‘ 𝐴 ) = 𝐿
7 6 eleq1i ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0 )
8 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) )
9 iftrue ⊢ ( 𝑁 ≤ 𝐿 → if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) = 𝑁 )
10 9 adantl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) = 𝑁 )
11 10 opeq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ = ⟨ 𝑀 , 𝑁 ⟩ )
12 11 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
13 iftrue ⊢ ( 0 ≤ ( 𝑀 − 𝐿 ) → if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) = ( 𝑀 − 𝐿 ) )
14 13 opeq1d ⊢ ( 0 ≤ ( 𝑀 − 𝐿 ) → ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ )
15 14 oveq2d ⊢ ( 0 ≤ ( 𝑀 − 𝐿 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
16 15 adantr ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
17 simpr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → 𝐵 ∈ Word 𝑉 )
18 nn0z ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ )
19 nn0z ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
20 19 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
21 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑀 − 𝐿 ) ∈ ℤ )
22 20 21 sylan ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℤ ) → ( 𝑀 − 𝐿 ) ∈ ℤ )
23 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
24 23 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℤ )
25 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
26 24 25 sylan ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℤ ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
27 22 26 jca ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℤ ) → ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
28 18 27 sylan2 ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
29 17 28 anim12i ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐵 ∈ Word 𝑉 ∧ ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) ) )
30 3anass ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) ↔ ( 𝐵 ∈ Word 𝑉 ∧ ( ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) ) )
31 29 30 sylibr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
32 31 ad2antrl ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
33 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
34 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
35 33 34 anim12i ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) )
36 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
37 subge0 ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
38 37 adantlr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
39 simpr ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑁 ∈ ℝ )
40 39 adantr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝑁 ∈ ℝ )
41 simpr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝐿 ∈ ℝ )
42 simpl ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → 𝑀 ∈ ℝ )
43 42 adantr ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → 𝑀 ∈ ℝ )
44 letr ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( ( 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 𝑁 ≤ 𝑀 ) )
45 40 41 43 44 syl3anc ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( ( 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 𝑁 ≤ 𝑀 ) )
46 45 expcomd ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 𝐿 ≤ 𝑀 → ( 𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀 ) ) )
47 38 46 sylbid ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 0 ≤ ( 𝑀 − 𝐿 ) → ( 𝑁 ≤ 𝐿 → 𝑁 ≤ 𝑀 ) ) )
48 47 com23 ⊢ ( ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) ∧ 𝐿 ∈ ℝ ) → ( 𝑁 ≤ 𝐿 → ( 0 ≤ ( 𝑀 − 𝐿 ) → 𝑁 ≤ 𝑀 ) ) )
49 35 36 48 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ≤ 𝐿 → ( 0 ≤ ( 𝑀 − 𝐿 ) → 𝑁 ≤ 𝑀 ) ) )
50 49 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑁 ≤ 𝐿 → ( 0 ≤ ( 𝑀 − 𝐿 ) → 𝑁 ≤ 𝑀 ) ) )
51 50 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 0 ≤ ( 𝑀 − 𝐿 ) → 𝑁 ≤ 𝑀 ) )
52 51 impcom ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → 𝑁 ≤ 𝑀 )
53 34 adantl ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
54 53 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑁 ∈ ℝ )
55 33 adantr ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
56 55 adantr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝑀 ∈ ℝ )
57 36 adantl ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℝ )
58 54 56 57 3jca ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
59 58 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
60 59 ad2antrl ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
61 lesub1 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑁 − 𝐿 ) ≤ ( 𝑀 − 𝐿 ) ) )
62 60 61 syl ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑁 − 𝐿 ) ≤ ( 𝑀 − 𝐿 ) ) )
63 52 62 mpbid ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝑁 − 𝐿 ) ≤ ( 𝑀 − 𝐿 ) )
64 swrdlend ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑀 − 𝐿 ) ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) → ( ( 𝑁 − 𝐿 ) ≤ ( 𝑀 − 𝐿 ) → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ ) )
65 32 63 64 sylc ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ )
66 16 65 eqtrd ⊢ ( ( 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ )
67 iffalse ⊢ ( ¬ 0 ≤ ( 𝑀 − 𝐿 ) → if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) = 0 )
68 67 opeq1d ⊢ ( ¬ 0 ≤ ( 𝑀 − 𝐿 ) → ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ = ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ )
69 68 oveq2d ⊢ ( ¬ 0 ≤ ( 𝑀 − 𝐿 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) )
70 17 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝐵 ∈ Word 𝑉 )
71 70 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → 𝐵 ∈ Word 𝑉 )
72 0zd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → 0 ∈ ℤ )
73 24 18 25 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
74 73 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
75 74 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑁 − 𝐿 ) ∈ ℤ )
76 71 72 75 3jca ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) )
77 53 36 anim12i ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
78 77 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) )
79 suble0 ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 𝑁 − 𝐿 ) ≤ 0 ↔ 𝑁 ≤ 𝐿 ) )
80 78 79 syl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝑁 − 𝐿 ) ≤ 0 ↔ 𝑁 ≤ 𝐿 ) )
81 80 biimpar ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝑁 − 𝐿 ) ≤ 0 )
82 swrdlend ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ ( 𝑁 − 𝐿 ) ∈ ℤ ) → ( ( 𝑁 − 𝐿 ) ≤ 0 → ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ ) )
83 76 81 82 sylc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ )
84 69 83 sylan9eq ⊢ ( ( ¬ 0 ≤ ( 𝑀 − 𝐿 ) ∧ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ )
85 66 84 pm2.61ian ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ∅ )
86 12 85 oveq12d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) )
87 swrdcl ⊢ ( 𝐴 ∈ Word 𝑉 → ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 )
88 ccatrid ⊢ ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ∈ Word 𝑉 → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
89 87 88 syl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
90 89 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
91 90 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
92 91 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) ++ ∅ ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
93 86 92 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝑁 ≤ 𝐿 ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) )
94 iffalse ⊢ ( ¬ 𝑁 ≤ 𝐿 → if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) = 𝐿 )
95 94 3ad2ant2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) = 𝐿 )
96 95 opeq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ = ⟨ 𝑀 , 𝐿 ⟩ )
97 96 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) )
98 simpl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → 𝐴 ∈ Word 𝑉 )
99 98 20 18 3anim123i ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
100 99 3expb ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) )
101 swrdlend ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ ) → ( 𝐿 ≤ 𝑀 → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) = ∅ ) )
102 100 101 syl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ≤ 𝑀 → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) = ∅ ) )
103 102 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 ≤ 𝑀 ) → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) = ∅ )
104 103 3adant2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) = ∅ )
105 97 104 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) = ∅ )
106 55 36 37 syl2an ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
107 106 biimprd ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐿 ≤ 𝑀 → 0 ≤ ( 𝑀 − 𝐿 ) ) )
108 107 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ≤ 𝑀 → 0 ≤ ( 𝑀 − 𝐿 ) ) )
109 108 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ 𝐿 ≤ 𝑀 ) → 0 ≤ ( 𝑀 − 𝐿 ) )
110 109 3adant2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → 0 ≤ ( 𝑀 − 𝐿 ) )
111 110 14 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ = ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ )
112 111 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
113 105 112 oveq12d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( ∅ ++ ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )
114 swrdcl ⊢ ( 𝐵 ∈ Word 𝑉 → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ∈ Word 𝑉 )
115 114 adantl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ∈ Word 𝑉 )
116 ccatlid ⊢ ( ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ∈ Word 𝑉 → ( ∅ ++ ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
117 115 116 syl ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ∅ ++ ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
118 117 adantr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ∅ ++ ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
119 118 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( ∅ ++ ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
120 113 119 eqtrd ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) )
121 94 3ad2ant2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) = 𝐿 )
122 121 opeq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ = ⟨ 𝑀 , 𝐿 ⟩ )
123 122 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) = ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) )
124 33 36 37 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
125 124 adantlr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
126 125 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 0 ≤ ( 𝑀 − 𝐿 ) ↔ 𝐿 ≤ 𝑀 ) )
127 126 biimpd ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 0 ≤ ( 𝑀 − 𝐿 ) → 𝐿 ≤ 𝑀 ) )
128 127 con3dimp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝐿 ≤ 𝑀 ) → ¬ 0 ≤ ( 𝑀 − 𝐿 ) )
129 128 3adant2 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ¬ 0 ≤ ( 𝑀 − 𝐿 ) )
130 129 67 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) = 0 )
131 130 opeq1d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ = ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ )
132 131 oveq2d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) )
133 70 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → 𝐵 ∈ Word 𝑉 )
134 simplrr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ) → 𝐿 ∈ ℕ0 )
135 simprlr ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝑁 ∈ ℕ0 )
136 135 adantr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ) → 𝑁 ∈ ℕ0 )
137 ltnle ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 < 𝑁 ↔ ¬ 𝑁 ≤ 𝐿 ) )
138 ltle ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐿 < 𝑁 → 𝐿 ≤ 𝑁 ) )
139 137 138 sylbird ⊢ ( ( 𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) )
140 36 53 139 syl2anr ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) )
141 140 adantl ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ¬ 𝑁 ≤ 𝐿 → 𝐿 ≤ 𝑁 ) )
142 141 imp ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ) → 𝐿 ≤ 𝑁 )
143 nn0sub2 ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ≤ 𝑁 ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 )
144 134 136 142 143 syl3anc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 )
145 144 3adant3 ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝑁 − 𝐿 ) ∈ ℕ0 )
146 133 145 jca ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑁 − 𝐿 ) ∈ ℕ0 ) )
147 pfxval ⊢ ( ( 𝐵 ∈ Word 𝑉 ∧ ( 𝑁 − 𝐿 ) ∈ ℕ0 ) → ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) = ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) )
148 146 147 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) = ( 𝐵 substr ⟨ 0 , ( 𝑁 − 𝐿 ) ⟩ ) )
149 132 148 eqtr4d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) = ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) )
150 123 149 oveq12d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) ∧ ¬ 𝑁 ≤ 𝐿 ∧ ¬ 𝐿 ≤ 𝑀 ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) )
151 93 120 150 2if2 ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
152 151 exp32 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 𝐿 ∈ ℕ0 → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
153 152 com12 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐿 ∈ ℕ0 → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
154 153 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ≤ 𝑁 ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐿 ∈ ℕ0 → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
155 8 154 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝑁 ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐿 ∈ ℕ0 → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
156 155 adantr ⊢ ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( 𝐿 ∈ ℕ0 → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
157 156 com13 ⊢ ( 𝐿 ∈ ℕ0 → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
158 7 157 sylbi ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) ) )
159 5 158 mpcom ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) ) )
160 159 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) = if ( 𝑁 ≤ 𝐿 , ( 𝐴 substr ⟨ 𝑀 , 𝑁 ⟩ ) , if ( 𝐿 ≤ 𝑀 , ( 𝐵 substr ⟨ ( 𝑀 − 𝐿 ) , ( 𝑁 − 𝐿 ) ⟩ ) , ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ++ ( 𝐵 prefix ( 𝑁 − 𝐿 ) ) ) ) ) )
161 3 160 eqtr4d ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) )
162 161 ex ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) = ( ( 𝐴 substr ⟨ 𝑀 , if ( 𝑁 ≤ 𝐿 , 𝑁 , 𝐿 ) ⟩ ) ++ ( 𝐵 substr ⟨ if ( 0 ≤ ( 𝑀 − 𝐿 ) , ( 𝑀 − 𝐿 ) , 0 ) , ( 𝑁 − 𝐿 ) ⟩ ) ) ) )