Proof of Theorem pfxccatpfx2
Step | Hyp | Ref
| Expression |
1 | | ccatcl 14129 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
2 | 1 | 3adant3 1134 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
3 | | swrdccatin2.l |
. . . . . . 7
⊢ 𝐿 = (♯‘𝐴) |
4 | | lencl 14088 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
5 | 3, 4 | eqeltrid 2842 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
6 | | elfzuz 13108 |
. . . . . 6
⊢ (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (ℤ≥‘(𝐿 + 1))) |
7 | | peano2nn0 12130 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) |
8 | 7 | anim1i 618 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
9 | 5, 6, 8 | syl2an 599 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
10 | 9 | 3adant2 1133 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
11 | | eluznn0 12513 |
. . . 4
⊢ (((𝐿 + 1) ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → 𝑁 ∈
ℕ0) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) |
13 | | pfxval 14238 |
. . 3
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
14 | 2, 12, 13 | syl2anc 587 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
15 | | 3simpa 1150 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
16 | 5 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) |
17 | | 0elfz 13209 |
. . . . 5
⊢ (𝐿 ∈ ℕ0
→ 0 ∈ (0...𝐿)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 0 ∈ (0...𝐿)) |
19 | 4 | nn0zd 12280 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) |
20 | 3, 19 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ) |
21 | 20 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ ℤ) |
22 | | uzid 12453 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
(ℤ≥‘𝐿)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ (ℤ≥‘𝐿)) |
24 | | peano2uz 12497 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐿) → (𝐿 + 1) ∈
(ℤ≥‘𝐿)) |
25 | | fzss1 13151 |
. . . . . . . 8
⊢ ((𝐿 + 1) ∈
(ℤ≥‘𝐿) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
27 | | pfxccatpfx2.m |
. . . . . . . . . 10
⊢ 𝑀 = (♯‘𝐵) |
28 | 27 | eqcomi 2746 |
. . . . . . . . 9
⊢
(♯‘𝐵) =
𝑀 |
29 | 28 | oveq2i 7224 |
. . . . . . . 8
⊢ (𝐿 + (♯‘𝐵)) = (𝐿 + 𝑀) |
30 | 29 | oveq2i 7224 |
. . . . . . 7
⊢ (𝐿...(𝐿 + (♯‘𝐵))) = (𝐿...(𝐿 + 𝑀)) |
31 | 26, 30 | sseqtrrdi 3952 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + (♯‘𝐵)))) |
32 | 31 | sseld 3900 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
33 | 32 | 3impia 1119 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) |
34 | 18, 33 | jca 515 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
35 | 3 | pfxccatin12 14298 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) |
36 | 15, 34, 35 | sylc 65 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) |
37 | 3 | opeq2i 4788 |
. . . . . 6
⊢ 〈0,
𝐿〉 = 〈0,
(♯‘𝐴)〉 |
38 | 37 | oveq2i 7224 |
. . . . 5
⊢ (𝐴 substr 〈0, 𝐿〉) = (𝐴 substr 〈0, (♯‘𝐴)〉) |
39 | | pfxval 14238 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ (♯‘𝐴) ∈ ℕ0) → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) |
40 | 4, 39 | mpdan 687 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) |
41 | | pfxid 14249 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = 𝐴) |
42 | 40, 41 | eqtr3d 2779 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (♯‘𝐴)〉) = 𝐴) |
43 | 38, 42 | syl5eq 2790 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
44 | 43 | 3ad2ant1 1135 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
45 | 44 | oveq1d 7228 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
46 | 14, 36, 45 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |