Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  swrdccat Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 swrdccatin2.l . . . . 5 𝐿 = (♯‘𝐴)
21pfxccat3 14157 . . . 4 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿)))))))
32imp 410 . . 3 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))
4 lencl 13946 . . . . . 6 (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
54adantr 484 . . . . 5 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (♯‘𝐴) ∈ ℕ0)
61eqcomi 2768 . . . . . . 7 (♯‘𝐴) = 𝐿
76eleq1i 2843 . . . . . 6 ((♯‘𝐴) ∈ ℕ0𝐿 ∈ ℕ0)
8 elfz2nn0 13061 . . . . . . . . 9 (𝑀 ∈ (0...𝑁) ↔ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑀𝑁))
9 iftrue 4430 . . . . . . . . . . . . . . . . . 18 (𝑁𝐿 → if(𝑁𝐿, 𝑁, 𝐿) = 𝑁)
109adantl 485 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → if(𝑁𝐿, 𝑁, 𝐿) = 𝑁)
1110opeq2d 4774 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝑁⟩)
1211oveq2d 7173 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝑁⟩))
13 iftrue 4430 . . . . . . . . . . . . . . . . . . . 20 (0 ≤ (𝑀𝐿) → if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0) = (𝑀𝐿))
1413opeq1d 4773 . . . . . . . . . . . . . . . . . . 19 (0 ≤ (𝑀𝐿) → ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩ = ⟨(𝑀𝐿), (𝑁𝐿)⟩)
1514oveq2d 7173 . . . . . . . . . . . . . . . . . 18 (0 ≤ (𝑀𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
1615adantr 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𝑀 ∈ ℤ)
2019adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑀 ∈ ℤ)
21 zsubcl 12077 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑀𝐿) ∈ ℤ)
2220, 21sylan 583 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑀𝐿) ∈ ℤ)
23 nn0z 12058 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ0𝑁 ∈ ℤ)
2423adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℤ)
25 zsubcl 12077 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
2624, 25sylan 583 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
2722, 26jca 515 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℤ) → ((𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ))
2818, 27sylan2 595 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → ((𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ))
2917, 28anim12i 615 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ ((𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ)))
30 3anass 1093 . . . . . . . . . . . . . . . . . . . 20 ((𝐵 ∈ Word 𝑉 ∧ (𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ) ↔ (𝐵 ∈ Word 𝑉 ∧ ((𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ)))
3129, 30sylibr 237 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ))
3231ad2antrl 727 . . . . . . . . . . . . . . . . . 18 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝐵 ∈ Word 𝑉 ∧ (𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ))
33 nn0re 11957 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑀 ∈ ℕ0𝑀 ∈ ℝ)
34 nn0re 11957 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ0𝑁 ∈ ℝ)
3533, 34anim12i 615 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ))
36 nn0re 11957 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
37 subge0 11205 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
3837adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
39 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑁 ∈ ℝ)
4039adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑁 ∈ ℝ)
41 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝐿 ∈ ℝ)
42 simpl 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → 𝑀 ∈ ℝ)
4342adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → 𝑀 ∈ ℝ)
44 letr 10786 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ 𝑀 ∈ ℝ) → ((𝑁𝐿𝐿𝑀) → 𝑁𝑀))
4540, 41, 43, 44syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → ((𝑁𝐿𝐿𝑀) → 𝑁𝑀))
4645expcomd 420 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝐿𝑀 → (𝑁𝐿𝑁𝑀)))
4738, 46sylbid 243 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑀𝐿) → (𝑁𝐿𝑁𝑀)))
4847com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) ∧ 𝐿 ∈ ℝ) → (𝑁𝐿 → (0 ≤ (𝑀𝐿) → 𝑁𝑀)))
4935, 36, 48syl2an 598 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁𝐿 → (0 ≤ (𝑀𝐿) → 𝑁𝑀)))
5049adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁𝐿 → (0 ≤ (𝑀𝐿) → 𝑁𝑀)))
5150imp 410 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (0 ≤ (𝑀𝐿) → 𝑁𝑀))
5251impcom 411 . . . . . . . . . . . . . . . . . . 19 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → 𝑁𝑀)
5334adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑁 ∈ ℝ)
5453adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑁 ∈ ℝ)
5533adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → 𝑀 ∈ ℝ)
5655adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝑀 ∈ ℝ)
5736adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℝ)
5854, 56, 573jca 1126 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
5958adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
6059ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ))
61 lesub1 11186 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑁𝑀 ↔ (𝑁𝐿) ≤ (𝑀𝐿)))
6260, 61syl 17 . . . . . . . . . . . . . . . . . . 19 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝑁𝑀 ↔ (𝑁𝐿) ≤ (𝑀𝐿)))
6352, 62mpbid 235 . . . . . . . . . . . . . . . . . 18 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝑁𝐿) ≤ (𝑀𝐿))
64 swrdlend 14076 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Word 𝑉 ∧ (𝑀𝐿) ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ) → ((𝑁𝐿) ≤ (𝑀𝐿) → (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩) = ∅))
6532, 63, 64sylc 65 . . . . . . . . . . . . . . . . 17 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩) = ∅)
6616, 65eqtrd 2794 . . . . . . . . . . . . . . . 16 ((0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = ∅)
67 iffalse 4433 . . . . . . . . . . . . . . . . . . 19 (¬ 0 ≤ (𝑀𝐿) → if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0) = 0)
6867opeq1d 4773 . . . . . . . . . . . . . . . . . 18 (¬ 0 ≤ (𝑀𝐿) → ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩ = ⟨0, (𝑁𝐿)⟩)
6968oveq2d 7173 . . . . . . . . . . . . . . . . 17 (¬ 0 ≤ (𝑀𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = (𝐵 substr ⟨0, (𝑁𝐿)⟩))
7017adantr 484 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → 𝐵 ∈ Word 𝑉)
7170adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → 𝐵 ∈ Word 𝑉)
72 0zd 12046 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → 0 ∈ ℤ)
7324, 18, 25syl2an 598 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁𝐿) ∈ ℤ)
7473adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁𝐿) ∈ ℤ)
7574adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝑁𝐿) ∈ ℤ)
7671, 72, 753jca 1126 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ))
7753, 36anim12i 615 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
7877adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ))
79 suble0 11206 . . . . . . . . . . . . . . . . . . . 20 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((𝑁𝐿) ≤ 0 ↔ 𝑁𝐿))
8078, 79syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝑁𝐿) ≤ 0 ↔ 𝑁𝐿))
8180biimpar 481 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝑁𝐿) ≤ 0)
82 swrdlend 14076 . . . . . . . . . . . . . . . . . 18 ((𝐵 ∈ Word 𝑉 ∧ 0 ∈ ℤ ∧ (𝑁𝐿) ∈ ℤ) → ((𝑁𝐿) ≤ 0 → (𝐵 substr ⟨0, (𝑁𝐿)⟩) = ∅))
8376, 81, 82sylc 65 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝐵 substr ⟨0, (𝑁𝐿)⟩) = ∅)
8469, 83sylan9eq 2814 . . . . . . . . . . . . . . . 16 ((¬ 0 ≤ (𝑀𝐿) ∧ (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿)) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = ∅)
8566, 84pm2.61ian 811 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = ∅)
8612, 85oveq12d 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 ⟨𝑀, 𝑁⟩))
8987, 88syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Word 𝑉 → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
9089adantr 484 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
9190adantr 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
9291adantr 484 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → ((𝐴 substr ⟨𝑀, 𝑁⟩) ++ ∅) = (𝐴 substr ⟨𝑀, 𝑁⟩))
9386, 92eqtrd 2794 . . . . . . . . . . . . 13 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝑁𝐿) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = (𝐴 substr ⟨𝑀, 𝑁⟩))
94 iffalse 4433 . . . . . . . . . . . . . . . . . . 19 𝑁𝐿 → if(𝑁𝐿, 𝑁, 𝐿) = 𝐿)
95943ad2ant2 1132 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → if(𝑁𝐿, 𝑁, 𝐿) = 𝐿)
9695opeq2d 4774 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
9796oveq2d 7173 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → (𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
98 simpl 486 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → 𝐴 ∈ Word 𝑉)
9998, 20, 183anim123i 1149 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐴 ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
100993expb 1118 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐴 ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ))
101 swrdlend 14076 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Word 𝑉𝑀 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
102100, 101syl 17 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿𝑀 → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅))
103102imp 410 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
1041033adant2 1129 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → (𝐴 substr ⟨𝑀, 𝐿⟩) = ∅)
10597, 104eqtrd 2794 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → (𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) = ∅)
10655, 36, 37syl2an 598 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
107106biimprd 251 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (𝐿𝑀 → 0 ≤ (𝑀𝐿)))
108107adantl 485 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (𝐿𝑀 → 0 ≤ (𝑀𝐿)))
109108imp 410 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ 𝐿𝑀) → 0 ≤ (𝑀𝐿))
1101093adant2 1129 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → 0 ≤ (𝑀𝐿))
111110, 14syl 17 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩ = ⟨(𝑀𝐿), (𝑁𝐿)⟩)
112111oveq2d 7173 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
113105, 112oveq12d 7175 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = (∅ ++ (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩)))
114 swrdcl 14068 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ Word 𝑉 → (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩) ∈ Word 𝑉)
115114adantl 485 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩) ∈ Word 𝑉)
116 ccatlid 14001 . . . . . . . . . . . . . . . . 17 ((𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩) ∈ Word 𝑉 → (∅ ++ (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩)) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
117115, 116syl 17 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (∅ ++ (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩)) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
118117adantr 484 . . . . . . . . . . . . . . 15 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (∅ ++ (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩)) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
1191183ad2ant1 1131 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → (∅ ++ (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩)) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
120113, 119eqtrd 2794 . . . . . . . . . . . . 13 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿𝐿𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩))
121943ad2ant2 1132 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → if(𝑁𝐿, 𝑁, 𝐿) = 𝐿)
122121opeq2d 4774 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩ = ⟨𝑀, 𝐿⟩)
123122oveq2d 7173 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) = (𝐴 substr ⟨𝑀, 𝐿⟩))
12433, 36, 37syl2an 598 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
125124adantlr 714 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
126125adantl 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀𝐿) ↔ 𝐿𝑀))
127126biimpd 232 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (0 ≤ (𝑀𝐿) → 𝐿𝑀))
128127con3dimp 412 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝐿𝑀) → ¬ 0 ≤ (𝑀𝐿))
1291283adant2 1129 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → ¬ 0 ≤ (𝑀𝐿))
130129, 67syl 17 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0) = 0)
131130opeq1d 4773 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩ = ⟨0, (𝑁𝐿)⟩)
132131oveq2d 7173 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = (𝐵 substr ⟨0, (𝑁𝐿)⟩))
133703ad2ant1 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)
136135adantr 484 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿) → 𝑁 ∈ ℕ0)
137 ltnle 10772 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁 ↔ ¬ 𝑁𝐿))
138 ltle 10781 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (𝐿 < 𝑁𝐿𝑁))
139137, 138sylbird 263 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐿 ∈ ℝ ∧ 𝑁 ∈ ℝ) → (¬ 𝑁𝐿𝐿𝑁))
14036, 53, 139syl2anr 599 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0) → (¬ 𝑁𝐿𝐿𝑁))
141140adantl 485 . . . . . . . . . . . . . . . . . . . 20 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → (¬ 𝑁𝐿𝐿𝑁))
142141imp 410 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿) → 𝐿𝑁)
143 nn0sub2 12096 . . . . . . . . . . . . . . . . . . 19 ((𝐿 ∈ ℕ0𝑁 ∈ ℕ0𝐿𝑁) → (𝑁𝐿) ∈ ℕ0)
144134, 136, 142, 143syl3anc 1369 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿) → (𝑁𝐿) ∈ ℕ0)
1451443adant3 1130 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝑁𝐿) ∈ ℕ0)
146133, 145jca 515 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝐵 ∈ Word 𝑉 ∧ (𝑁𝐿) ∈ ℕ0))
147 pfxval 14096 . . . . . . . . . . . . . . . 16 ((𝐵 ∈ Word 𝑉 ∧ (𝑁𝐿) ∈ ℕ0) → (𝐵 prefix (𝑁𝐿)) = (𝐵 substr ⟨0, (𝑁𝐿)⟩))
148146, 147syl 17 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝐵 prefix (𝑁𝐿)) = (𝐵 substr ⟨0, (𝑁𝐿)⟩))
149132, 148eqtr4d 2797 . . . . . . . . . . . . . 14 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩) = (𝐵 prefix (𝑁𝐿)))
150123, 149oveq12d 7175 . . . . . . . . . . . . 13 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) ∧ ¬ 𝑁𝐿 ∧ ¬ 𝐿𝑀) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))
15193, 120, 1502if2 4479 . . . . . . . . . . . 12 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))
152151exp32 424 . . . . . . . . . . 11 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
153152com12 32 . . . . . . . . . 10 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
1541533adant3 1130 . . . . . . . . 9 ((𝑀 ∈ ℕ0𝑁 ∈ ℕ0𝑀𝑁) → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
1558, 154sylbi 220 . . . . . . . 8 (𝑀 ∈ (0...𝑁) → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
156155adantr 484 . . . . . . 7 ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → (𝐿 ∈ ℕ0 → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
157156com13 88 . . . . . 6 (𝐿 ∈ ℕ0 → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
1587, 157sylbi 220 . . . . 5 ((♯‘𝐴) ∈ ℕ0 → ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))))
1595, 158mpcom 38 . . . 4 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿)))))))
160159imp 410 . . 3 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)) = if(𝑁𝐿, (𝐴 substr ⟨𝑀, 𝑁⟩), if(𝐿𝑀, (𝐵 substr ⟨(𝑀𝐿), (𝑁𝐿)⟩), ((𝐴 substr ⟨𝑀, 𝐿⟩) ++ (𝐵 prefix (𝑁𝐿))))))
1613, 160eqtr4d 2797 . 2 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩)))
162161ex 416 1 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩) = ((𝐴 substr ⟨𝑀, if(𝑁𝐿, 𝑁, 𝐿)⟩) ++ (𝐵 substr ⟨if(0 ≤ (𝑀𝐿), (𝑀𝐿), 0), (𝑁𝐿)⟩))))
 Colors of variables: wff setvar class 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  ℕ0cn0 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)
 Copyright terms: Public domain W3C validator