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

Theorem pfxccatin12lem3 14441
Description: Lemma 3 for pfxccatin12 14442. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
Hypothesis
Ref Expression
swrdccatin2.l 𝐿 = (♯‘𝐴)
Assertion
Ref Expression
pfxccatin12lem3 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾)))

Proof of Theorem pfxccatin12lem3
StepHypRef Expression
1 simpll 764 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉))
2 elfzo0 13424 . . . . . . . . 9 (𝐾 ∈ (0..^(𝐿𝑀)) ↔ (𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)))
3 swrdccatin2.l . . . . . . . . . . . . 13 𝐿 = (♯‘𝐴)
4 lencl 14232 . . . . . . . . . . . . 13 (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℕ0)
5 elfz2nn0 13344 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ (0...𝐿) ↔ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿))
6 nn0addcl 12266 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0𝑀 ∈ ℕ0) → (𝐾 + 𝑀) ∈ ℕ0)
76ex 413 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐾 ∈ ℕ0 → (𝑀 ∈ ℕ0 → (𝐾 + 𝑀) ∈ ℕ0))
873ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → (𝑀 ∈ ℕ0 → (𝐾 + 𝑀) ∈ ℕ0))
98com12 32 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑀 ∈ ℕ0 → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → (𝐾 + 𝑀) ∈ ℕ0))
1093ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → (𝐾 + 𝑀) ∈ ℕ0))
1110imp 407 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) ∧ (𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀))) → (𝐾 + 𝑀) ∈ ℕ0)
12 elnnz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐿𝑀) ∈ ℕ ↔ ((𝐿𝑀) ∈ ℤ ∧ 0 < (𝐿𝑀)))
13 nn0re 12240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ ℕ0𝑀 ∈ ℝ)
14 nn0re 12240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝐿 ∈ ℕ0𝐿 ∈ ℝ)
15 posdif 11466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → (𝑀 < 𝐿 ↔ 0 < (𝐿𝑀)))
1613, 14, 15syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑀 < 𝐿 ↔ 0 < (𝐿𝑀)))
17 elnn0z 12330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑀 ∈ ℕ0 ↔ (𝑀 ∈ ℤ ∧ 0 ≤ 𝑀))
18 0re 10976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 0 ∈ ℝ
19 zre 12321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
20 lelttr 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((0 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝐿 ∈ ℝ) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
2118, 19, 14, 20mp3an3an 1466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0) → ((0 ≤ 𝑀𝑀 < 𝐿) → 0 < 𝐿))
22 nn0z 12341 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝐿 ∈ ℕ0𝐿 ∈ ℤ)
2322anim1i 615 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐿 ∈ ℕ0 ∧ 0 < 𝐿) → (𝐿 ∈ ℤ ∧ 0 < 𝐿))
24 elnnz 12327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝐿 ∈ ℕ ↔ (𝐿 ∈ ℤ ∧ 0 < 𝐿))
2523, 24sylibr 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐿 ∈ ℕ0 ∧ 0 < 𝐿) → 𝐿 ∈ ℕ)
2625ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐿 ∈ ℕ0 → (0 < 𝐿𝐿 ∈ ℕ))
2726adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0) → (0 < 𝐿𝐿 ∈ ℕ))
2821, 27syld 47 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0) → ((0 ≤ 𝑀𝑀 < 𝐿) → 𝐿 ∈ ℕ))
2928expd 416 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝑀 ∈ ℤ ∧ 𝐿 ∈ ℕ0) → (0 ≤ 𝑀 → (𝑀 < 𝐿𝐿 ∈ ℕ)))
3029impancom 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝑀 ∈ ℤ ∧ 0 ≤ 𝑀) → (𝐿 ∈ ℕ0 → (𝑀 < 𝐿𝐿 ∈ ℕ)))
3117, 30sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑀 ∈ ℕ0 → (𝐿 ∈ ℕ0 → (𝑀 < 𝐿𝐿 ∈ ℕ)))
3231imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (𝑀 < 𝐿𝐿 ∈ ℕ))
3316, 32sylbird 259 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → (0 < (𝐿𝑀) → 𝐿 ∈ ℕ))
3433com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 < (𝐿𝑀) → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → 𝐿 ∈ ℕ))
3512, 34simplbiim 505 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐿𝑀) ∈ ℕ → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → 𝐿 ∈ ℕ))
36353ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → 𝐿 ∈ ℕ))
3736com12 32 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → 𝐿 ∈ ℕ))
38373adant3 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → 𝐿 ∈ ℕ))
3938imp 407 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) ∧ (𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀))) → 𝐿 ∈ ℕ)
40 nn0re 12240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐾 ∈ ℕ0𝐾 ∈ ℝ)
4140adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿)) → 𝐾 ∈ ℝ)
42133ad2ant1 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → 𝑀 ∈ ℝ)
4342adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿)) → 𝑀 ∈ ℝ)
44143ad2ant2 1133 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → 𝐿 ∈ ℝ)
4544adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿)) → 𝐿 ∈ ℝ)
4641, 43, 45ltaddsubd 11573 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ ℕ0 ∧ (𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿)) → ((𝐾 + 𝑀) < 𝐿𝐾 < (𝐿𝑀)))
4746exbiri 808 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐾 ∈ ℕ0 → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 < (𝐿𝑀) → (𝐾 + 𝑀) < 𝐿)))
4847com23 86 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐾 ∈ ℕ0 → (𝐾 < (𝐿𝑀) → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 + 𝑀) < 𝐿)))
4948imp 407 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐾 ∈ ℕ0𝐾 < (𝐿𝑀)) → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 + 𝑀) < 𝐿))
50493adant2 1130 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝐾 + 𝑀) < 𝐿))
5150impcom 408 . . . . . . . . . . . . . . . . . . . . 21 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) ∧ (𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀))) → (𝐾 + 𝑀) < 𝐿)
5211, 39, 513jca 1127 . . . . . . . . . . . . . . . . . . . 20 (((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) ∧ (𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀))) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))
5352ex 413 . . . . . . . . . . . . . . . . . . 19 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))
5453a1d 25 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∈ ℕ0𝐿 ∈ ℕ0𝑀𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))
555, 54sylbi 216 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ (0...𝐿) → (𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))
5655imp 407 . . . . . . . . . . . . . . . 16 ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))
57562a1i 12 . . . . . . . . . . . . . . 15 ((♯‘𝐴) = 𝐿 → (𝐿 ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))))
58 eleq1 2828 . . . . . . . . . . . . . . 15 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴) ∈ ℕ0𝐿 ∈ ℕ0))
59 eleq1 2828 . . . . . . . . . . . . . . . . . 18 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴) ∈ ℕ ↔ 𝐿 ∈ ℕ))
60 breq2 5083 . . . . . . . . . . . . . . . . . 18 ((♯‘𝐴) = 𝐿 → ((𝐾 + 𝑀) < (♯‘𝐴) ↔ (𝐾 + 𝑀) < 𝐿))
6159, 603anbi23d 1438 . . . . . . . . . . . . . . . . 17 ((♯‘𝐴) = 𝐿 → (((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))
6261imbi2d 341 . . . . . . . . . . . . . . . 16 ((♯‘𝐴) = 𝐿 → (((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))) ↔ ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿))))
6362imbi2d 341 . . . . . . . . . . . . . . 15 ((♯‘𝐴) = 𝐿 → (((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))) ↔ ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0𝐿 ∈ ℕ ∧ (𝐾 + 𝑀) < 𝐿)))))
6457, 58, 633imtr4d 294 . . . . . . . . . . . . . 14 ((♯‘𝐴) = 𝐿 → ((♯‘𝐴) ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))))
6564eqcoms 2748 . . . . . . . . . . . . 13 (𝐿 = (♯‘𝐴) → ((♯‘𝐴) ∈ ℕ0 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))))
663, 4, 65mpsyl 68 . . . . . . . . . . . 12 (𝐴 ∈ Word 𝑉 → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))))
6766adantr 481 . . . . . . . . . . 11 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) → ((𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))))
6867imp 407 . . . . . . . . . 10 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))
6968com12 32 . . . . . . . . 9 ((𝐾 ∈ ℕ0 ∧ (𝐿𝑀) ∈ ℕ ∧ 𝐾 < (𝐿𝑀)) → (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))
702, 69sylbi 216 . . . . . . . 8 (𝐾 ∈ (0..^(𝐿𝑀)) → (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))
7170adantl 482 . . . . . . 7 ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴))))
7271impcom 408 . . . . . 6 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))
73 elfzo0 13424 . . . . . 6 ((𝐾 + 𝑀) ∈ (0..^(♯‘𝐴)) ↔ ((𝐾 + 𝑀) ∈ ℕ0 ∧ (♯‘𝐴) ∈ ℕ ∧ (𝐾 + 𝑀) < (♯‘𝐴)))
7472, 73sylibr 233 . . . . 5 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴)))
75 df-3an 1088 . . . . 5 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))) ↔ ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))))
761, 74, 75sylanbrc 583 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → (𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))))
77 ccatval1 14277 . . . 4 ((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉 ∧ (𝐾 + 𝑀) ∈ (0..^(♯‘𝐴))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀)))
7876, 77syl 17 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)) = (𝐴‘(𝐾 + 𝑀)))
793pfxccatin12lem2c 14439 . . . 4 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
80 simpl 483 . . . 4 ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀))) → 𝐾 ∈ (0..^(𝑁𝑀)))
81 swrdfv 14357 . . . 4 ((((𝐴 ++ 𝐵) ∈ Word 𝑉𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))) ∧ 𝐾 ∈ (0..^(𝑁𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
8279, 80, 81syl2an 596 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 ++ 𝐵)‘(𝐾 + 𝑀)))
83 simplll 772 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐴 ∈ Word 𝑉)
84 simplrl 774 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝑀 ∈ (0...𝐿))
853eleq1i 2831 . . . . . . 7 (𝐿 ∈ ℕ0 ↔ (♯‘𝐴) ∈ ℕ0)
86 elnn0uz 12620 . . . . . . . . 9 (𝐿 ∈ ℕ0𝐿 ∈ (ℤ‘0))
87 eluzfz2 13261 . . . . . . . . 9 (𝐿 ∈ (ℤ‘0) → 𝐿 ∈ (0...𝐿))
8886, 87sylbi 216 . . . . . . . 8 (𝐿 ∈ ℕ0𝐿 ∈ (0...𝐿))
893oveq2i 7280 . . . . . . . 8 (0...𝐿) = (0...(♯‘𝐴))
9088, 89eleqtrdi 2851 . . . . . . 7 (𝐿 ∈ ℕ0𝐿 ∈ (0...(♯‘𝐴)))
9185, 90sylbir 234 . . . . . 6 ((♯‘𝐴) ∈ ℕ0𝐿 ∈ (0...(♯‘𝐴)))
924, 91syl 17 . . . . 5 (𝐴 ∈ Word 𝑉𝐿 ∈ (0...(♯‘𝐴)))
9392ad3antrrr 727 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐿 ∈ (0...(♯‘𝐴)))
94 simprr 770 . . . 4 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → 𝐾 ∈ (0..^(𝐿𝑀)))
95 swrdfv 14357 . . . 4 (((𝐴 ∈ Word 𝑉𝑀 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝐴))) ∧ 𝐾 ∈ (0..^(𝐿𝑀))) → ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾) = (𝐴‘(𝐾 + 𝑀)))
9683, 84, 93, 94, 95syl31anc 1372 . . 3 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾) = (𝐴‘(𝐾 + 𝑀)))
9778, 82, 963eqtr4d 2790 . 2 ((((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) ∧ (𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀)))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾))
9897ex 413 1 (((𝐴 ∈ Word 𝑉𝐵 ∈ Word 𝑉) ∧ (𝑀 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) → ((𝐾 ∈ (0..^(𝑁𝑀)) ∧ 𝐾 ∈ (0..^(𝐿𝑀))) → (((𝐴 ++ 𝐵) substr ⟨𝑀, 𝑁⟩)‘𝐾) = ((𝐴 substr ⟨𝑀, 𝐿⟩)‘𝐾)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  cop 4573   class class class wbr 5079  cfv 6431  (class class class)co 7269  cr 10869  0cc0 10870   + caddc 10873   < clt 11008  cle 11009  cmin 11203  cn 11971  0cn0 12231  cz 12317  cuz 12579  ...cfz 13236  ..^cfzo 13379  chash 14040  Word cword 14213   ++ cconcat 14269   substr csubstr 14349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7580  ax-cnex 10926  ax-resscn 10927  ax-1cn 10928  ax-icn 10929  ax-addcl 10930  ax-addrcl 10931  ax-mulcl 10932  ax-mulrcl 10933  ax-mulcom 10934  ax-addass 10935  ax-mulass 10936  ax-distr 10937  ax-i2m1 10938  ax-1ne0 10939  ax-1rid 10940  ax-rnegex 10941  ax-rrecex 10942  ax-cnre 10943  ax-pre-lttri 10944  ax-pre-lttrn 10945  ax-pre-ltadd 10946  ax-pre-mulgt0 10947
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-nel 3052  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-int 4886  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-tr 5197  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6200  df-ord 6267  df-on 6268  df-lim 6269  df-suc 6270  df-iota 6389  df-fun 6433  df-fn 6434  df-f 6435  df-f1 6436  df-fo 6437  df-f1o 6438  df-fv 6439  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-om 7705  df-1st 7822  df-2nd 7823  df-frecs 8086  df-wrecs 8117  df-recs 8191  df-rdg 8230  df-1o 8286  df-er 8479  df-en 8715  df-dom 8716  df-sdom 8717  df-fin 8718  df-card 9696  df-pnf 11010  df-mnf 11011  df-xr 11012  df-ltxr 11013  df-le 11014  df-sub 11205  df-neg 11206  df-nn 11972  df-n0 12232  df-z 12318  df-uz 12580  df-fz 13237  df-fzo 13380  df-hash 14041  df-word 14214  df-concat 14270  df-substr 14350
This theorem is referenced by:  pfxccatin12  14442
  Copyright terms: Public domain W3C validator