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

Metamath Proof Explorer

Theorem pfxccatin12lem3

Description: Lemma 3 for pfxccatin12 . (Contributed by AV, 30-Mar-2018) (Revised by AV, 27-May-2018)

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

Proof

Step Hyp Ref Expression
1 swrdccatin2.l ⊢ 𝐿 = ( ♯ ‘ 𝐴 )
2 simpll ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) )
3 elfzo0 ⊢ ( 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ↔ ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) )
4 lencl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
5 elfz2nn0 ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) ↔ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) )
6 nn0addcl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 + 𝑀 ) ∈ ℕ0 )
7 6 ex ⊢ ( 𝐾 ∈ ℕ0 → ( 𝑀 ∈ ℕ0 → ( 𝐾 + 𝑀 ) ∈ ℕ0 ) )
8 7 3ad2ant1 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( 𝑀 ∈ ℕ0 → ( 𝐾 + 𝑀 ) ∈ ℕ0 ) )
9 8 com12 ⊢ ( 𝑀 ∈ ℕ0 → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ℕ0 ) )
10 9 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( 𝐾 + 𝑀 ) ∈ ℕ0 ) )
11 10 imp ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) ∈ ℕ0 )
12 elnnz ⊢ ( ( 𝐿 − 𝑀 ) ∈ ℕ ↔ ( ( 𝐿 − 𝑀 ) ∈ ℤ ∧ 0 < ( 𝐿 − 𝑀 ) ) )
13 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
14 nn0re ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℝ )
15 posdif ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( 𝑀 < 𝐿 ↔ 0 < ( 𝐿 − 𝑀 ) ) )
16 13 14 15 syl2an ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 ↔ 0 < ( 𝐿 − 𝑀 ) ) )
17 elnn0z ⊢ ( 𝑀 ∈ ℕ0 ↔ ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) )
18 0re ⊢ 0 ∈ ℝ
19 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
20 lelttr ⊢ ( ( 0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 < 𝐿 ) → 0 < 𝐿 ) )
21 18 19 14 20 mp3an3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0 ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 < 𝐿 ) → 0 < 𝐿 ) )
22 nn0z ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ℤ )
23 22 anim1i ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 0 < 𝐿 ) → ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) )
24 elnnz ⊢ ( 𝐿 ∈ ℕ ↔ ( 𝐿 ∈ ℤ ∧ 0 < 𝐿 ) )
25 23 24 sylibr ⊢ ( ( 𝐿 ∈ ℕ0 ∧ 0 < 𝐿 ) → 𝐿 ∈ ℕ )
26 25 ex ⊢ ( 𝐿 ∈ ℕ0 → ( 0 < 𝐿 → 𝐿 ∈ ℕ ) )
27 26 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0 ) → ( 0 < 𝐿 → 𝐿 ∈ ℕ ) )
28 21 27 syld ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0 ) → ( ( 0 ≤ 𝑀 ∧ 𝑀 < 𝐿 ) → 𝐿 ∈ ℕ ) )
29 28 expd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0 ) → ( 0 ≤ 𝑀 → ( 𝑀 < 𝐿 → 𝐿 ∈ ℕ ) ) )
30 29 impancom ⊢ ( ( 𝑀 ∈ ℤ ∧ 0 ≤ 𝑀 ) → ( 𝐿 ∈ ℕ0 → ( 𝑀 < 𝐿 → 𝐿 ∈ ℕ ) ) )
31 17 30 sylbi ⊢ ( 𝑀 ∈ ℕ0 → ( 𝐿 ∈ ℕ0 → ( 𝑀 < 𝐿 → 𝐿 ∈ ℕ ) ) )
32 31 imp ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 𝑀 < 𝐿 → 𝐿 ∈ ℕ ) )
33 16 32 sylbird ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( 0 < ( 𝐿 − 𝑀 ) → 𝐿 ∈ ℕ ) )
34 33 com12 ⊢ ( 0 < ( 𝐿 − 𝑀 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ ) )
35 12 34 simplbiim ⊢ ( ( 𝐿 − 𝑀 ) ∈ ℕ → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ ) )
36 35 3ad2ant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → 𝐿 ∈ ℕ ) )
37 36 com12 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → 𝐿 ∈ ℕ ) )
38 37 3adant3 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → 𝐿 ∈ ℕ ) )
39 38 imp ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) ) → 𝐿 ∈ ℕ )
40 nn0re ⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℝ )
41 40 adantr ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ) → 𝐾 ∈ ℝ )
42 13 3ad2ant1 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → 𝑀 ∈ ℝ )
43 42 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ) → 𝑀 ∈ ℝ )
44 14 3ad2ant2 ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → 𝐿 ∈ ℝ )
45 44 adantl ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ) → 𝐿 ∈ ℝ )
46 41 43 45 ltaddsubd ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ) → ( ( 𝐾 + 𝑀 ) < 𝐿 ↔ 𝐾 < ( 𝐿 − 𝑀 ) ) )
47 46 exbiri ⊢ ( 𝐾 ∈ ℕ0 → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝐾 < ( 𝐿 − 𝑀 ) → ( 𝐾 + 𝑀 ) < 𝐿 ) ) )
48 47 com23 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 < ( 𝐿 − 𝑀 ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝐾 + 𝑀 ) < 𝐿 ) ) )
49 48 imp ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝐾 + 𝑀 ) < 𝐿 ) )
50 49 3adant2 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝐾 + 𝑀 ) < 𝐿 ) )
51 50 impcom ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) ) → ( 𝐾 + 𝑀 ) < 𝐿 )
52 11 39 51 3jca ⊢ ( ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) ∧ ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) )
53 52 ex ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) )
54 53 a1d ⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ≤ 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) ) )
55 5 54 sylbi ⊢ ( 𝑀 ∈ ( 0 ... 𝐿 ) → ( 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) ) )
56 55 imp ⊢ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) )
57 56 2a1i ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( 𝐿 ∈ ℕ0 → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) ) ) )
58 eleq1 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ 𝐿 ∈ ℕ0 ) )
59 eleq1 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 𝐿 ∈ ℕ ) )
60 breq2 ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ↔ ( 𝐾 + 𝑀 ) < 𝐿 ) )
61 59 60 3anbi23d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ↔ ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) )
62 61 imbi2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ↔ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) ) )
63 62 imbi2d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) ↔ ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < 𝐿 ) ) ) ) )
64 57 58 63 3imtr4d ⊢ ( ( ♯ ‘ 𝐴 ) = 𝐿 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) ) )
65 64 eqcoms ⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) ) )
66 1 4 65 mpsyl ⊢ ( 𝐴 ∈ Word 𝑉 → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) )
67 66 adantr ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) → ( ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) ) )
68 67 imp ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
69 68 com12 ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐿 − 𝑀 ) ∈ ℕ ∧ 𝐾 < ( 𝐿 − 𝑀 ) ) → ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
70 3 69 sylbi ⊢ ( 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) → ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
71 70 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) ) )
72 71 impcom ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
73 elfzo0 ⊢ ( ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ( 𝐾 + 𝑀 ) ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ( 𝐾 + 𝑀 ) < ( ♯ ‘ 𝐴 ) ) )
74 72 73 sylibr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
75 df-3an ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) ↔ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) )
76 2 74 75 sylanbrc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) )
77 ccatval1 ⊢ ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ ( 𝐾 + 𝑀 ) ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) = ( 𝐴 ‘ ( 𝐾 + 𝑀 ) ) )
78 76 77 syl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) = ( 𝐴 ‘ ( 𝐾 + 𝑀 ) ) )
79 1 pfxccatin12lem2c ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) )
80 simpl ⊢ ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) )
81 swrdfv ⊢ ( ( ( ( 𝐴 ++ 𝐵 ) ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝑁 ) ∧ 𝑁 ∈ ( 0 ... ( ♯ ‘ ( 𝐴 ++ 𝐵 ) ) ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) )
82 79 80 81 syl2an ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 ++ 𝐵 ) ‘ ( 𝐾 + 𝑀 ) ) )
83 simplll ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐴 ∈ Word 𝑉 )
84 simplrl ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝑀 ∈ ( 0 ... 𝐿 ) )
85 1 eleq1i ⊢ ( 𝐿 ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
86 elnn0uz ⊢ ( 𝐿 ∈ ℕ0 ↔ 𝐿 ∈ ( ℤ≥ ‘ 0 ) )
87 eluzfz2 ⊢ ( 𝐿 ∈ ( ℤ≥ ‘ 0 ) → 𝐿 ∈ ( 0 ... 𝐿 ) )
88 86 87 sylbi ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ( 0 ... 𝐿 ) )
89 1 oveq2i ⊢ ( 0 ... 𝐿 ) = ( 0 ... ( ♯ ‘ 𝐴 ) )
90 88 89 eleqtrdi ⊢ ( 𝐿 ∈ ℕ0 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
91 85 90 sylbir ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
92 4 91 syl ⊢ ( 𝐴 ∈ Word 𝑉 → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
93 92 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) )
94 simprr ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) )
95 swrdfv ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝐿 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝐾 ) = ( 𝐴 ‘ ( 𝐾 + 𝑀 ) ) )
96 83 84 93 94 95 syl31anc ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝐾 ) = ( 𝐴 ‘ ( 𝐾 + 𝑀 ) ) )
97 78 82 96 3eqtr4d ⊢ ( ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) ∧ ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝐾 ) )
98 97 ex ⊢ ( ( ( 𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ) ∧ ( 𝑀 ∈ ( 0 ... 𝐿 ) ∧ 𝑁 ∈ ( 𝐿 ... ( 𝐿 + ( ♯ ‘ 𝐵 ) ) ) ) ) → ( ( 𝐾 ∈ ( 0 ..^ ( 𝑁 − 𝑀 ) ) ∧ 𝐾 ∈ ( 0 ..^ ( 𝐿 − 𝑀 ) ) ) → ( ( ( 𝐴 ++ 𝐵 ) substr ⟨ 𝑀 , 𝑁 ⟩ ) ‘ 𝐾 ) = ( ( 𝐴 substr ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝐾 ) ) )