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

Theorem pfxccatin12lem2 14329
Description: Lemma 2 for pfxccatin12 14331. (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 14328 . . . 4 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
3 simprl 771 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐾 ∈ (0..^(𝑁𝑀)))
4 swrdfv 14246 . . . 4 ((((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝐾 ∈ (0..^(𝑁𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
52, 3, 4syl2an2r 685 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
6 elfzoelz 13273 . . . . . . . 8 (𝐾 ∈ (0..^(𝑁𝑀)) → 𝐾 ∈ ℤ)
7 elfz2nn0 13233 . . . . . . . . . 10 (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿))
8 nn0cn 12130 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ0𝑀 ∈ ℂ)
9 nn0cn 12130 . . . . . . . . . . . . . . . 16 (𝐿 ∈ ℕ0𝐿 ∈ ℂ)
108, 9anim12i 616 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ))
11 zcn 12211 . . . . . . . . . . . . . . 15 (𝐾 ∈ ℤ → 𝐾 ∈ ℂ)
12 subcl 11107 . . . . . . . . . . . . . . . . . . . 20 ((𝐿 ∈ ℂ ∧ 𝑀 ∈ ℂ) → (𝐿𝑀) ∈ ℂ)
1312ancoms 462 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) → (𝐿𝑀) ∈ ℂ)
1413anim1ci 619 . . . . . . . . . . . . . . . . . 18 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 ∈ ℂ ∧ (𝐿𝑀) ∈ ℂ))
15 subcl 11107 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℂ ∧ (𝐿𝑀) ∈ ℂ) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
1614, 15syl 17 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
1716addid1d 11062 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → ((𝐾 − (𝐿𝑀)) + 0) = (𝐾 − (𝐿𝑀)))
18 simpr 488 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝐾 ∈ ℂ)
19 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝐿 ∈ ℂ)
20 simpll 767 . . . . . . . . . . . . . . . . 17 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → 𝑀 ∈ ℂ)
2118, 19, 20subsub3d 11249 . . . . . . . . . . . . . . . 16 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → (𝐾 − (𝐿𝑀)) = ((𝐾 + 𝑀) − 𝐿))
2217, 21eqtr2d 2780 . . . . . . . . . . . . . . 15 (((𝑀 ∈ ℂ ∧ 𝐿 ∈ ℂ) ∧ 𝐾 ∈ ℂ) → ((𝐾 + 𝑀) − 𝐿) = ((𝐾 − (𝐿𝑀)) + 0))
2310, 11, 22syl2an 599 . . . . . . . . . . . . . 14 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) ∧ 𝐾 ∈ ℤ) → ((𝐾 + 𝑀) − 𝐿) = ((𝐾 − (𝐿𝑀)) + 0))
24 oveq2 7243 . . . . . . . . . . . . . . . 16 ((♯‘𝐴) = 𝐿 → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 + 𝑀) − 𝐿))
2524eqcoms 2747 . . . . . . . . . . . . . . 15 (𝐿 = (♯‘𝐴) → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 + 𝑀) − 𝐿))
2625eqeq1d 2741 . . . . . . . . . . . . . 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 1134 . . . . . . . . . 10 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
317, 30sylbi 220 . . . . . . . . 9 (𝑀 ∈ (0...𝐿) → (𝐾 ∈ ℤ → ((𝐾 + 𝑀) − (♯‘𝐴)) = ((𝐾 − (𝐿𝑀)) + 0)))
3231ad2antrl 728 . . . . . . . 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 6743 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
37 simpll 767 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉))
38 pfxccatin12lem2a 14325 . . . . . . . . 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 7242 . . . . . . . . . . 11 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴) + (♯‘𝐵)) = (𝐿 + (♯‘𝐵)))
4341, 42oveq12d 7253 . . . . . . . . . 10 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) = (𝐿..^(𝐿 + (♯‘𝐵))))
4443eleq2d 2825 . . . . . . . . 9 ((♯‘𝐴) = 𝐿 → ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
4544eqcoms 2747 . . . . . . . 8 (𝐿 = (♯‘𝐴) → ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵)))))
461, 45ax-mp 5 . . . . . . 7 ((𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))) ↔ (𝐾 + 𝑀) ∈ (𝐿..^(𝐿 + (♯‘𝐵))))
4740, 46sylibr 237 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵))))
48 df-3an 1091 . . . . . 6 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) ↔ ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
4937, 47, 48sylanbrc 586 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))))
50 ccatval2 14168 . . . . 5 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ ((♯‘𝐴)..^((♯‘𝐴) + (♯‘𝐵)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))))
5149, 50syl 17 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐵‘((𝐾 + 𝑀) − (♯‘𝐴))))
52 simplr 769 . . . . . . 7 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐵 ∈ Word 𝑉)
5352adantr 484 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐵 ∈ Word 𝑉)
54 lencl 14121 . . . . . . . . . 10 (𝐵 ∈ Word 𝑉 → (♯‘𝐵) ∈ ℕ0)
55 elfzel2 13140 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝐿 ∈ ℤ)
56 zsubcl 12249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑁 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
5756ancoms 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁𝐿) ∈ ℤ)
5857adantr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐿𝑁) → (𝑁𝐿) ∈ ℤ)
59 zre 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
60 zre 12210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝐿 ∈ ℤ → 𝐿 ∈ ℝ)
61 subge0 11375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (0 ≤ (𝑁𝐿) ↔ 𝐿𝑁))
6259, 60, 61syl2anr 600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (0 ≤ (𝑁𝐿) ↔ 𝐿𝑁))
6362biimprd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐿𝑁 → 0 ≤ (𝑁𝐿)))
6463imp 410 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝐿 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝐿𝑁) → 0 ≤ (𝑁𝐿))
65 elnn0z 12219 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1137 . . . . . . . . . . . . . . . . . . . . 21 ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))) → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0)))
7271imp 410 . . . . . . . . . . . . . . . . . . . 20 (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝐿 ∈ ℤ → (𝑁𝐿) ∈ ℕ0))
7372com12 32 . . . . . . . . . . . . . . . . . . 19 (𝐿 ∈ ℤ → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ ℕ0))
7473adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → (𝑁𝐿) ∈ ℕ0))
7574imp 410 . . . . . . . . . . . . . . . . 17 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → (𝑁𝐿) ∈ ℕ0)
76 simplr 769 . . . . . . . . . . . . . . . . 17 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → (♯‘𝐵) ∈ ℕ0)
77593ad2ant3 1137 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
7877adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝑁 ∈ ℝ)
7960adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → 𝐿 ∈ ℝ)
8079adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → 𝐿 ∈ ℝ)
81 nn0re 12129 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((♯‘𝐵) ∈ ℕ0 → (♯‘𝐵) ∈ ℝ)
8281adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (♯‘𝐵) ∈ ℝ)
8382adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ (𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ)) → (♯‘𝐵) ∈ ℝ)
84 lesubadd2 11335 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → ((𝑁𝐿) ≤ (♯‘𝐵) ↔ 𝑁 ≤ (𝐿 + (♯‘𝐵))))
8584biimprd 251 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℝ ∧ 𝐿 ∈ ℝ ∧ (♯‘𝐵) ∈ ℝ) → (𝑁 ≤ (𝐿 + (♯‘𝐵)) → (𝑁𝐿) ≤ (♯‘𝐵)))
8678, 80, 83, 85syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 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 1130 . . . . . . . . . . . . . . . 16 (((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) ∧ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵))))) → ((𝑁𝐿) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (𝑁𝐿) ≤ (♯‘𝐵)))
9392ex 416 . . . . . . . . . . . . . . 15 ((𝐿 ∈ ℤ ∧ (♯‘𝐵) ∈ ℕ0) → (((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))) → ((𝑁𝐿) ∈ ℕ0 ∧ (♯‘𝐵) ∈ ℕ0 ∧ (𝑁𝐿) ≤ (♯‘𝐵))))
94 elfz2 13132 . . . . . . . . . . . . . . 15 (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) ↔ ((𝐿 ∈ ℤ ∧ (𝐿 + (♯‘𝐵)) ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐿𝑁𝑁 ≤ (𝐿 + (♯‘𝐵)))))
95 elfz2nn0 13233 . . . . . . . . . . . . . . 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 14326 . . . . . . . 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 14280 . . . . . 6 ((𝐵 ∈ Word 𝑉 ∧ (𝑁𝐿) ∈ (0...(♯‘𝐵)) ∧ (𝐾 − (𝐿𝑀)) ∈ (0..^(𝑁𝐿))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘(𝐾 − (𝐿𝑀))))
10953, 104, 107, 108syl3anc 1373 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘(𝐾 − (𝐿𝑀))))
1106zcnd 12313 . . . . . . . . . 10 (𝐾 ∈ (0..^(𝑁𝑀)) → 𝐾 ∈ ℂ)
111110ad2antrl 728 . . . . . . . . 9 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐾 ∈ ℂ)
11255zcnd 12313 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝐿 ∈ ℂ)
113112ad2antrl 728 . . . . . . . . . . 11 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐿 ∈ ℂ)
114113adantr 484 . . . . . . . . . 10 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐿 ∈ ℂ)
115 elfzelz 13142 . . . . . . . . . . . . 13 (𝑀 ∈ (0...𝐿) → 𝑀 ∈ ℤ)
116115zcnd 12313 . . . . . . . . . . . 12 (𝑀 ∈ (0...𝐿) → 𝑀 ∈ ℂ)
117116ad2antrl 728 . . . . . . . . . . 11 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ ℂ)
118117adantr 484 . . . . . . . . . 10 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝑀 ∈ ℂ)
119114, 118subcld 11219 . . . . . . . . 9 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐿𝑀) ∈ ℂ)
120111, 119subcld 11219 . . . . . . . 8 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) ∈ ℂ)
121120addid1d 11062 . . . . . . 7 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐾 − (𝐿𝑀)) + 0) = (𝐾 − (𝐿𝑀)))
122121eqcomd 2745 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) = ((𝐾 − (𝐿𝑀)) + 0))
123122fveq2d 6743 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐵‘(𝐾 − (𝐿𝑀))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
124109, 123eqtrd 2779 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = (𝐵‘((𝐾 − (𝐿𝑀)) + 0)))
12536, 51, 1243eqtr4d 2789 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))))
126 simpll 767 . . . . . . . . 9 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝐴 ∈ Word 𝑉)
127 simprl 771 . . . . . . . . 9 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → 𝑀 ∈ (0...𝐿))
128 lencl 14121 . . . . . . . . . . . 12 (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
129 elnn0uz 12509 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ ℕ0 ↔ (♯‘𝐴) ∈ (ℤ‘0))
130 eluzfz2 13150 . . . . . . . . . . . . . 14 ((♯‘𝐴) ∈ (ℤ‘0) → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
131129, 130sylbi 220 . . . . . . . . . . . . 13 ((♯‘𝐴) ∈ ℕ0 → (♯‘𝐴) ∈ (0...(♯‘𝐴)))
1321, 131eqeltrid 2844 . . . . . . . . . . . 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 1130 . . . . . . . 8 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → (𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))))
137136adantr 484 . . . . . . 7 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))))
138 swrdlen 14245 . . . . . . 7 ((𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿𝑀))
139137, 138syl 17 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)) = (𝐿𝑀))
140139eqcomd 2745 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐿𝑀) = (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))
141140oveq2d 7251 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 − (𝐿𝑀)) = (𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩))))
142141fveq2d 6743 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ ¬ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (𝐿𝑀))) = ((𝐵 prefix (𝑁𝐿))‘(𝐾 − (♯‘(𝐴 substr ⟨𝑀, 𝐿⟩)))))
1435, 125, 1423eqtrd 2783 . 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 1089   = wceq 1543  wcel 2112  cop 4564   class class class wbr 5070  cfv 6401  (class class class)co 7235  cc 10757  cr 10758  0cc0 10759   + caddc 10762  cle 10898  cmin 11092  0cn0 12120  cz 12206  cuz 12468  ...cfz 13125  ..^cfzo 13268  chash 13929  Word cword 14102   ++ cconcat 14158   substr csubstr 14238   prefix cpfx 14268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5196  ax-sep 5209  ax-nul 5216  ax-pow 5275  ax-pr 5339  ax-un 7545  ax-cnex 10815  ax-resscn 10816  ax-1cn 10817  ax-icn 10818  ax-addcl 10819  ax-addrcl 10820  ax-mulcl 10821  ax-mulrcl 10822  ax-mulcom 10823  ax-addass 10824  ax-mulass 10825  ax-distr 10826  ax-i2m1 10827  ax-1ne0 10828  ax-1rid 10829  ax-rnegex 10830  ax-rrecex 10831  ax-cnre 10832  ax-pre-lttri 10833  ax-pre-lttrn 10834  ax-pre-ltadd 10835  ax-pre-mulgt0 10836
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5179  df-id 5472  df-eprel 5478  df-po 5486  df-so 5487  df-fr 5527  df-we 5529  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-pred 6179  df-ord 6237  df-on 6238  df-lim 6239  df-suc 6240  df-iota 6359  df-fun 6403  df-fn 6404  df-f 6405  df-f1 6406  df-fo 6407  df-f1o 6408  df-fv 6409  df-riota 7192  df-ov 7238  df-oprab 7239  df-mpo 7240  df-om 7667  df-1st 7783  df-2nd 7784  df-wrecs 8071  df-recs 8132  df-rdg 8170  df-1o 8226  df-er 8415  df-en 8651  df-dom 8652  df-sdom 8653  df-fin 8654  df-card 9585  df-pnf 10899  df-mnf 10900  df-xr 10901  df-ltxr 10902  df-le 10903  df-sub 11094  df-neg 11095  df-nn 11861  df-n0 12121  df-z 12207  df-uz 12469  df-fz 13126  df-fzo 13269  df-hash 13930  df-word 14103  df-concat 14159  df-substr 14239  df-pfx 14269
This theorem is referenced by:  pfxccatin12  14331
  Copyright terms: Public domain W3C validator