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

Theorem pfxccatin12lem2 14084
Description: Lemma 2 for pfxccatin12 14086. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
Hypothesis
Ref Expression
swrdccatin2.l 𝐿 = (♯‘𝐴)
Assertion
Ref Expression
pfxccatin12lem2 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))

Proof of Theorem pfxccatin12lem2
StepHypRef Expression
1 swrdccatin2.l . . . . 5 𝐿 = (♯‘𝐴)
21pfxccatin12lem2c 14083 . . . 4 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
3 simprl 770 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐾 ∈ (0..^(𝑁𝑀)))
4 swrdfv 14001 . . . 4 ((((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝐾 ∈ (0..^(𝑁𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
52, 3, 4syl2an2r 684 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
6 elfzoelz 13033 . . . . . . . 8 (𝐾 ∈ (0..^(𝑁𝑀)) → 𝐾 ∈ ℤ)
7 elfz2nn0 12993 . . . . . . . . . 10 (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿))
8 nn0cn 11895 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0𝑀 ∈ ℂ)
9 nn0cn 11895 . . . . . . . . . . . . . . . 16 (𝐿 ∈ ℕ0𝐿 ∈ ℂ)
108, 9anim12i 615 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ))
11 zcn 11974 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
12 subcl 10874 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐿𝑀) ∈ ℂ)
1312ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿𝑀) ∈ ℂ)
1413anim1ci 618 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 ∈ ℂ ∧ (𝐿𝑀) ∈ ℂ))
15 subcl 10874 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℂ ∧ (𝐿𝑀) ∈ ℂ) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
1614, 15syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
1716addid1d 10829 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → ((𝐾 − (𝐿𝑀)) + 0) = (𝐾 − (𝐿𝑀)))
18 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝐾 ∈ ℂ)
19 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝐿 ∈ ℂ)
20 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝑀 ∈ ℂ)
2118, 19, 20subsub3d 11016 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 − (𝐿𝑀)) = ((𝐾 + 𝑀) − 𝐿))
2217, 21eqtr2d 2858 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → ((𝐾 + 𝑀) − 𝐿) = ((𝐾 − (𝐿𝑀)) + 0))
2310, 11, 22syl2an 598 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) ∧ 𝐾 ∈ ℤ) → ((𝐾 + 𝑀) − 𝐿) = ((𝐾 − (𝐿𝑀)) + 0))
24 oveq2 7148 . . . . . . . . . . . . . . . 16 ((♯‘𝐴) = 𝐿 → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 + 𝑀) − 𝐿))
2524eqcoms 2830 . . . . . . . . . . . . . . 15 (𝐿 = (♯‘𝐴) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 + 𝑀) − 𝐿))
2625eqeq1d 2824 . . . . . . . . . . . . . 14 (𝐿 = (♯‘𝐴) → (((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0) ↔ ((𝐾 + 𝑀) − 𝐿) = ((𝐾 − (𝐿𝑀)) + 0)))
2723, 26syl5ibr 249 . . . . . . . . . . . . 13 (𝐿 = (♯‘𝐴) → (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) ∧ 𝐾 ∈ ℤ) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
281, 27ax-mp 5 . . . . . . . . . . . 12 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) ∧ 𝐾 ∈ ℤ) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0))
2928ex 416 . . . . . . . . . . 11 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
30293adant3 1129 . . . . . . . . . 10 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
317, 30sylbi 220 . . . . . . . . 9 (𝑀 ∈ (0...𝐿) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
3231ad2antrl 727 . . . . . . . 8 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
336, 32syl5com 31 . . . . . . 7 (𝐾 ∈ (0..^(𝑁𝑀)) → (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
3433adantr 484 . . . . . 6 ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
3534impcom 411 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0))
3635fveq2d 6656 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
37 simpll 766 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉))
38 pfxccatin12lem2a 14080 . . . . . . . . 9 ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
3938adantl 485 . . . . . . . 8 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
4039imp 410 . . . . . . 7 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵))))
41 id 22 . . . . . . . . . . 11 ((♯‘𝐴) = 𝐿 → (♯‘𝐴) = 𝐿)
42 oveq1 7147 . . . . . . . . . . 11 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴) + (♯‘𝐵)) = (𝐿 + (♯‘𝐵)))
4341, 42oveq12d 7158 . . . . . . . . . 10 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) = (𝐿..^(𝐿 + (♯‘𝐵))))
4443eleq2d 2899 . . . . . . . . 9 ((♯‘𝐴) = 𝐿 → ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
4544eqcoms 2830 . . . . . . . 8 (𝐿 = (♯‘𝐴) → ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
461, 45ax-mp 5 . . . . . . 7 ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵))))
4740, 46sylibr 237 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
48 df-3an 1086 . . . . . 6 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) ↔ ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
4937, 47, 48sylanbrc 586 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
50 ccatval2 13923 . . . . 5 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))))
5149, 50syl 17 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))))
52 simplr 768 . . . . . . 7 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐵 ∈ Word 𝑉)
5352adantr 484 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐵 ∈ Word 𝑉)
54 lencl 13876 . . . . . . . . . 10 (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ0)
55 elfzel2 12900 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
56 zsubcl 12012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
5756ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
5857adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐿𝑁) → (𝑁𝐿) ∈ ℤ)
59 zre 11973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
60 zre 11973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
61 subge0 11142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑁𝐿) ↔ 𝐿𝑁))
6259, 60, 61syl2anr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑁𝐿) ↔ 𝐿𝑁))
6362biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 → 0 ≤ (𝑁𝐿)))
6463imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐿𝑁) → 0 ≤ (𝑁𝐿))
65 elnn0z 11982 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑁𝐿) ∈ ℕ0 ↔ ((𝑁𝐿) ∈ ℤ ∧ 0 ≤ (𝑁𝐿)))
6658, 64, 65sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐿𝑁) → (𝑁𝐿) ∈ ℕ0)
6766expcom 417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐿𝑁 → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝐿) ∈ ℕ0))
6867adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝐿) ∈ ℕ0))
6968expcomd 420 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → (𝑁 ∈ ℤ → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0)))
7069com12 32 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℤ → ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0)))
71703ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0)))
7271imp 410 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0))
7372com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐿 ∈ ℤ → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ ℕ0))
7473adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ ℕ0))
7574imp 410 . . . . . . . . . . . . . . . . 17 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → (𝑁𝐿) ∈ ℕ0)
76 simplr 768 . . . . . . . . . . . . . . . . 17 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → (♯‘𝐵) ∈ ℕ0)
77593ad2ant3 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
7877adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
7960adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → 𝐿 ∈ ℝ)
8079adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝐿 ∈ ℝ)
81 nn0re 11894 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝐵) ∈ ℕ0 → (♯‘𝐵) ∈ ℝ)
8281adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐵) ∈ ℝ)
8382adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (♯‘𝐵) ∈ ℝ)
84 lesubadd2 11102 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → ((𝑁𝐿) ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝐿 + (♯‘𝐵))))
8584biimprd 251 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → (𝑁 ≤ (𝐿 + (♯‘𝐵)) → (𝑁𝐿) ≤ (♯‘𝐵)))
8678, 80, 83, 85syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (𝑁 ≤ (𝐿 + (♯‘𝐵)) → (𝑁𝐿) ≤ (♯‘𝐵)))
8786ex 416 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ≤ (𝐿 + (♯‘𝐵)) → (𝑁𝐿) ≤ (♯‘𝐵))))
8887com13 88 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ≤ (𝐿 + (♯‘𝐵)) → ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (𝑁𝐿) ≤ (♯‘𝐵))))
8988adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (𝑁𝐿) ≤ (♯‘𝐵))))
9089impcom 411 . . . . . . . . . . . . . . . . . 18 (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (𝑁𝐿) ≤ (♯‘𝐵)))
9190impcom 411 . . . . . . . . . . . . . . . . 17 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → (𝑁𝐿) ≤ (♯‘𝐵))
9275, 76, 913jca 1125 . . . . . . . . . . . . . . . 16 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → ((𝑁𝐿) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (𝑁𝐿) ≤ (♯‘𝐵)))
9392ex 416 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → ((𝑁𝐿) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (𝑁𝐿) ≤ (♯‘𝐵))))
94 elfz2 12892 . . . . . . . . . . . . . . 15 (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) ↔ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))))
95 elfz2nn0 12993 . . . . . . . . . . . . . . 15 ((𝑁𝐿) ∈ (0...(♯‘𝐵)) ↔ ((𝑁𝐿) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (𝑁𝐿) ≤ (♯‘𝐵)))
9693, 94, 953imtr4g 299 . . . . . . . . . . . . . 14 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝑁𝐿) ∈ (0...(♯‘𝐵))))
9796ex 416 . . . . . . . . . . . . 13 (𝐿 ∈ ℤ → ((♯‘𝐵) ∈ ℕ0 → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → (𝑁𝐿) ∈ (0...(♯‘𝐵)))))
9897com23 86 . . . . . . . . . . . 12 (𝐿 ∈ ℤ → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((♯‘𝐵) ∈ ℕ0 → (𝑁𝐿) ∈ (0...(♯‘𝐵)))))
9955, 98syl 17 . . . . . . . . . . 11 (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((♯‘𝐵) ∈ ℕ0 → (𝑁𝐿) ∈ (0...(♯‘𝐵)))))
10099imp 410 . . . . . . . . . 10 ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((♯‘𝐵) ∈ ℕ0 → (𝑁𝐿) ∈ (0...(♯‘𝐵))))
10154, 100syl5com 31 . . . . . . . . 9 (𝐵 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ (0...(♯‘𝐵))))
102101adantl 485 . . . . . . . 8 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ (0...(♯‘𝐵))))
103102imp 410 . . . . . . 7 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝑁𝐿) ∈ (0...(♯‘𝐵)))
104103adantr 484 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝑁𝐿) ∈ (0...(♯‘𝐵)))
105 pfxccatin12lem1 14081 . . . . . . . 8 ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (𝐾 − (𝐿𝑀)) ∈ (0..^(𝑁𝐿))))
106105adantl 485 . . . . . . 7 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (𝐾 − (𝐿𝑀)) ∈ (0..^(𝑁𝐿))))
107106imp 410 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) ∈ (0..^(𝑁𝐿)))
108 pfxfv 14035 . . . . . 6 ((𝐵 ∈ Word 𝑉 ∧ (𝑁𝐿) ∈ (0...(♯‘𝐵)) ∧ (𝐾 − (𝐿𝑀)) ∈ (0..^(𝑁𝐿))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘(𝐾 − (𝐿𝑀))))
10953, 104, 107, 108syl3anc 1368 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘(𝐾 − (𝐿𝑀))))
1106zcnd 12076 . . . . . . . . . 10 (𝐾 ∈ (0..^(𝑁𝑀)) → 𝐾 ∈ ℂ)
111110ad2antrl 727 . . . . . . . . 9 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐾 ∈ ℂ)
11255zcnd 12076 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝐿 ∈ ℂ)
113112ad2antrl 727 . . . . . . . . . . 11 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ ℂ)
114113adantr 484 . . . . . . . . . 10 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐿 ∈ ℂ)
115 elfzelz 12902 . . . . . . . . . . . . 13 (𝑀 ∈ (0...𝐿) → 𝑀 ∈ ℤ)
116115zcnd 12076 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝑀 ∈ ℂ)
117116ad2antrl 727 . . . . . . . . . . 11 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ ℂ)
118117adantr 484 . . . . . . . . . 10 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝑀 ∈ ℂ)
119114, 118subcld 10986 . . . . . . . . 9 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐿𝑀) ∈ ℂ)
120111, 119subcld 10986 . . . . . . . 8 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
121120addid1d 10829 . . . . . . 7 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐾 − (𝐿𝑀)) + 0) = (𝐾 − (𝐿𝑀)))
122121eqcomd 2828 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) = ((𝐾 − (𝐿𝑀)) + 0))
123122fveq2d 6656 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐵‘(𝐾 − (𝐿𝑀))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
124109, 123eqtrd 2857 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
12536, 51, 1243eqtr4d 2867 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))))
126 simpll 766 . . . . . . . . 9 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐴 ∈ Word 𝑉)
127 simprl 770 . . . . . . . . 9 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ (0...𝐿))
128 lencl 13876 . . . . . . . . . . . 12 (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
129 elnn0uz 12271 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ ℕ0 ↔ (♯‘𝐴) ∈ (ℤ‘0))
130 eluzfz2 12910 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ (ℤ‘0) → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
131129, 130sylbi 220 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
1321, 131eqeltrid 2918 . . . . . . . . . . . 12 ((♯‘𝐴) ∈ ℕ0𝐿 ∈ (0...(♯‘𝐴)))
133128, 132syl 17 . . . . . . . . . . 11 (𝐴 ∈ Word 𝑉𝐿 ∈ (0...(♯‘𝐴)))
134133adantr 484 . . . . . . . . . 10 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → 𝐿 ∈ (0...(♯‘𝐴)))
135134adantr 484 . . . . . . . . 9 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ (0...(♯‘𝐴)))
136126, 127, 1353jca 1125 . . . . . . . 8 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))))
137136adantr 484 . . . . . . 7 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))))
138 swrdlen 14000 . . . . . . 7 ((𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿𝑀))
139137, 138syl 17 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿𝑀))
140139eqcomd 2828 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐿𝑀) = (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))
141140oveq2d 7156 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) = (𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))
142141fveq2d 6656 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
1435, 125, 1423eqtrd 2861 . 2 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
144143ex 416 1 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  cop 4545   class class class wbr 5042  cfv 6334  (class class class)co 7140  cc 10524  cr 10525  0cc0 10526   + caddc 10529  cle 10665  cmin 10859  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  ..^cfzo 13028  chash 13686  Word cword 13857   ++ cconcat 13913   substr csubstr 13993   prefix cpfx 14023
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970  df-uz 12232  df-fz 12886  df-fzo 13029  df-hash 13687  df-word 13858  df-concat 13914  df-substr 13994  df-pfx 14024
This theorem is referenced by:  pfxccatin12  14086
  Copyright terms: Public domain W3C validator