Proof of Theorem pfxccatpfx2
Step | Hyp | Ref
| Expression |
1 | | ccatcl 13212 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
2 | 1 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
3 | | pfxccatin12.l |
. . . . . . 7
⊢ 𝐿 = (#‘𝐴) |
4 | | lencl 13179 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈
ℕ0) |
5 | 3, 4 | syl5eqel 2692 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
6 | | elfzuz 12209 |
. . . . . 6
⊢ (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (ℤ≥‘(𝐿 + 1))) |
7 | | peano2nn0 11210 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) |
8 | 7 | anim1i 590 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
9 | 5, 6, 8 | syl2an 493 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
10 | 9 | 3adant2 1073 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
11 | | eluznn0 11633 |
. . . 4
⊢ (((𝐿 + 1) ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → 𝑁 ∈
ℕ0) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) |
13 | | pfxval 40246 |
. . 3
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
14 | 2, 12, 13 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) |
15 | | 3simpa 1051 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
16 | 5 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) |
17 | | 0elfz 12305 |
. . . . 5
⊢ (𝐿 ∈ ℕ0
→ 0 ∈ (0...𝐿)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 0 ∈ (0...𝐿)) |
19 | 4 | nn0zd 11356 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (#‘𝐴) ∈ ℤ) |
20 | 3, 19 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ) |
21 | 20 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ ℤ) |
22 | | uzid 11578 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
(ℤ≥‘𝐿)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ (ℤ≥‘𝐿)) |
24 | | peano2uz 11617 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐿) → (𝐿 + 1) ∈
(ℤ≥‘𝐿)) |
25 | | fzss1 12251 |
. . . . . . . 8
⊢ ((𝐿 + 1) ∈
(ℤ≥‘𝐿) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
26 | 23, 24, 25 | 3syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) |
27 | | pfxccatpfx2.m |
. . . . . . . . . 10
⊢ 𝑀 = (#‘𝐵) |
28 | 27 | eqcomi 2619 |
. . . . . . . . 9
⊢
(#‘𝐵) = 𝑀 |
29 | 28 | oveq2i 6560 |
. . . . . . . 8
⊢ (𝐿 + (#‘𝐵)) = (𝐿 + 𝑀) |
30 | 29 | oveq2i 6560 |
. . . . . . 7
⊢ (𝐿...(𝐿 + (#‘𝐵))) = (𝐿...(𝐿 + 𝑀)) |
31 | 26, 30 | syl6sseqr 3615 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + (#‘𝐵)))) |
32 | 31 | sseld 3567 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) |
33 | 32 | 3impia 1253 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) |
34 | 18, 33 | jca 553 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵))))) |
35 | 3 | pfxccatin12 40288 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (#‘𝐵)))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))))) |
36 | 15, 34, 35 | sylc 63 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉) = ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿)))) |
37 | 3 | opeq2i 4344 |
. . . . . 6
⊢ 〈0,
𝐿〉 = 〈0,
(#‘𝐴)〉 |
38 | 37 | oveq2i 6560 |
. . . . 5
⊢ (𝐴 substr 〈0, 𝐿〉) = (𝐴 substr 〈0, (#‘𝐴)〉) |
39 | | swrdid 13280 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (#‘𝐴)〉) = 𝐴) |
40 | 38, 39 | syl5eq 2656 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
41 | 40 | 3ad2ant1 1075 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 substr 〈0, 𝐿〉) = 𝐴) |
42 | 41 | oveq1d 6564 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
43 | 14, 36, 42 | 3eqtrd 2648 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |