Theorem swrdccat 14158

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.)

Hypothesis

Ref	Expression
swrdccatin2.l	⊢ 𝐿 = (♯‘𝐴)

Assertion

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

Proof of Theorem swrdccat

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∅c0 4228  ifcif 4424  ⟨cop 4532   class class class wbr 5037  ‘cfv 6341  (class class class)co 7157  ℝcr 10588  0cc0 10589   + caddc 10592   < clt 10727   ≤ cle 10728   − cmin 10922  ℕ₀cn0 11948  ℤcz 12034  ...cfz 12953  ♯chash 13754  Word cword 13927   ++ cconcat 13983   substr csubstr 14063   prefix cpfx 14093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5161  ax-sep 5174  ax-nul 5181  ax-pow 5239  ax-pr 5303  ax-un 7466  ax-cnex 10645  ax-resscn 10646  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-mulcom 10653  ax-addass 10654  ax-mulass 10655  ax-distr 10656  ax-i2m1 10657  ax-1ne0 10658  ax-1rid 10659  ax-rnegex 10660  ax-rrecex 10661  ax-cnre 10662  ax-pre-lttri 10663  ax-pre-lttrn 10664  ax-pre-ltadd 10665  ax-pre-mulgt0 10666

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-int 4843  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7115  df-ov 7160  df-oprab 7161  df-mpo 7162  df-om 7587  df-1st 7700  df-2nd 7701  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-1o 8119  df-er 8306  df-en 8542  df-dom 8543  df-sdom 8544  df-fin 8545  df-card 9415  df-pnf 10729  df-mnf 10730  df-xr 10731  df-ltxr 10732  df-le 10733  df-sub 10924  df-neg 10925  df-nn 11689  df-n0 11949  df-z 12035  df-uz 12297  df-fz 12954  df-fzo 13097  df-hash 13755  df-word 13928  df-concat 13984  df-substr 14064  df-pfx 14094

This theorem is referenced by: (None)