Proof of Theorem pfxccatpfx2
Step | Hyp | Ref
| Expression |
1 | | ccatcl 14584 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
2 | 1 | 3adant3 1129 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
3 | | swrdccatin2.l |
. . . . . . 7
⊢ 𝐿 = (♯‘𝐴) |
4 | | lencl 14543 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
5 | 3, 4 | eqeltrid 2830 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
6 | | elfzuz 13553 |
. . . . . 6
⊢ (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (ℤ≥‘(𝐿 + 1))) |
7 | | peano2nn0 12566 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) |
8 | 7 | anim1i 613 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
9 | 5, 6, 8 | syl2an 594 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
10 | 9 | 3adant2 1128 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
11 | | eluznn0 12955 |
. . . 4
⊢ (((𝐿 + 1) ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → 𝑁 ∈
ℕ0) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) |
13 | | pfxval 14683 |
. . 3
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
14 | 2, 12, 13 | syl2anc 582 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
15 | | 3simpa 1145 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
16 | 5 | 3ad2ant1 1130 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) |
17 | | 0elfz 13654 |
. . . . 5
⊢ (𝐿 ∈ ℕ0
→ 0 ∈ (0...𝐿)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 0 ∈ (0...𝐿)) |
19 | 4 | nn0zd 12638 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) |
20 | 3, 19 | eqeltrid 2830 |
. . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ) |
21 | 20 | adantr 479 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ ℤ) |
22 | | uzid 12891 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
(ℤ≥‘𝐿)) |
23 | | peano2uz 12939 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐿) → (𝐿 + 1) ∈
(ℤ≥‘𝐿)) |
24 | | fzss1 13596 |
. . . . . . . 8
⊢ ((𝐿 + 1) ∈
(ℤ≥‘𝐿) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
25 | 21, 22, 23, 24 | 4syl 19 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
26 | | pfxccatpfx2.m |
. . . . . . . . . 10
⊢ 𝑀 = (♯‘𝐵) |
27 | 26 | eqcomi 2735 |
. . . . . . . . 9
⊢
(♯‘𝐵) =
𝑀 |
28 | 27 | oveq2i 7437 |
. . . . . . . 8
⊢ (𝐿 + (♯‘𝐵)) = (𝐿 + 𝑀) |
29 | 28 | oveq2i 7437 |
. . . . . . 7
⊢ (𝐿...(𝐿 + (♯‘𝐵))) = (𝐿...(𝐿 + 𝑀)) |
30 | 25, 29 | sseqtrrdi 4031 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + (♯‘𝐵)))) |
31 | 30 | sseld 3978 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
32 | 31 | 3impia 1114 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) |
33 | 18, 32 | jca 510 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
34 | 3 | pfxccatin12 14743 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) |
35 | 15, 33, 34 | sylc 65 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) |
36 | 3 | opeq2i 4885 |
. . . . . 6
⊢ 〈0,
𝐿〉 = 〈0,
(♯‘𝐴)〉 |
37 | 36 | oveq2i 7437 |
. . . . 5
⊢ (𝐴 substr 〈0, 𝐿〉) = (𝐴 substr 〈0, (♯‘𝐴)〉) |
38 | | pfxval 14683 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ (♯‘𝐴) ∈ ℕ0) → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) |
39 | 4, 38 | mpdan 685 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) |
40 | | pfxid 14694 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = 𝐴) |
41 | 39, 40 | eqtr3d 2768 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (♯‘𝐴)〉) = 𝐴) |
42 | 37, 41 | eqtrid 2778 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
43 | 42 | 3ad2ant1 1130 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
44 | 43 | oveq1d 7441 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
45 | 14, 35, 44 | 3eqtrd 2770 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |