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 ⟨ 𝑀 , 𝐿 ⟩ ) ‘ 𝐾 ) ) )