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	addid1d	⊢ ( ( ( 𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ ) ∧ 𝐾 ∈ ℂ ) → ( ( 𝐾 − ( 𝐿 − 𝑀 ) ) + 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	syl5ibr	⊢ ( 𝐿 = ( ♯ ‘ 𝐴 ) → ( ( ( 𝑀 ∈ ℕ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	addid1d	⊢ ( ( ( ( 𝐴 ∈ 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 ⟨ 𝑀 , 𝐿 ⟩ ) ) ) ) ) )