Step | Hyp | Ref
| Expression |
1 | | ccatcl 14469 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
2 | 1 | 3adant3 1133 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) |
3 | | swrdccatin2.l |
. . . . . . 7
⊢ 𝐿 = (♯‘𝐴) |
4 | | lencl 14428 |
. . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) |
5 | 3, 4 | eqeltrid 2842 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) |
6 | | elfzuz 13444 |
. . . . . 6
⊢ (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (ℤ≥‘(𝐿 + 1))) |
7 | | peano2nn0 12460 |
. . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) |
8 | 7 | anim1i 616 |
. . . . . 6
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
9 | 5, 6, 8 | syl2an 597 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
10 | 9 | 3adant2 1132 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) |
11 | | eluznn0 12849 |
. . . 4
⊢ (((𝐿 + 1) ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → 𝑁 ∈
ℕ0) |
12 | 10, 11 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) |
13 | | pfxval 14568 |
. . 3
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr ⟨0, 𝑁⟩)) |
14 | 2, 12, 13 | syl2anc 585 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr ⟨0, 𝑁⟩)) |
15 | | 3simpa 1149 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) |
16 | 5 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) |
17 | | 0elfz 13545 |
. . . . 5
⊢ (𝐿 ∈ ℕ0
→ 0 ∈ (0...𝐿)) |
18 | 16, 17 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 0 ∈ (0...𝐿)) |
19 | 4 | nn0zd 12532 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) |
20 | 3, 19 | eqeltrid 2842 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ) |
21 | 20 | adantr 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ ℤ) |
22 | | uzid 12785 |
. . . . . . . . 9
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
(ℤ≥‘𝐿)) |
23 | 21, 22 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ (ℤ≥‘𝐿)) |
24 | | peano2uz 12833 |
. . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐿) → (𝐿 + 1) ∈
(ℤ≥‘𝐿)) |
25 | | fzss1 13487 |
. . . . . . . 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 7373 |
. . . . . . . 8
⊢ (𝐿 + (♯‘𝐵)) = (𝐿 + 𝑀) |
30 | 29 | oveq2i 7373 |
. . . . . . 7
⊢ (𝐿...(𝐿 + (♯‘𝐵))) = (𝐿...(𝐿 + 𝑀)) |
31 | 26, 30 | sseqtrrdi 4000 |
. . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + (♯‘𝐵)))) |
32 | 31 | sseld 3948 |
. . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
33 | 32 | 3impia 1118 |
. . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) |
34 | 18, 33 | jca 513 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) |
35 | 3 | pfxccatin12 14628 |
. . 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 4839 |
. . . . . 6
⊢ ⟨0,
𝐿⟩ = ⟨0,
(♯‘𝐴)⟩ |
38 | 37 | oveq2i 7373 |
. . . . 5
⊢ (𝐴 substr ⟨0, 𝐿⟩) = (𝐴 substr ⟨0, (♯‘𝐴)⟩) |
39 | | pfxval 14568 |
. . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ (♯‘𝐴) ∈ ℕ0) → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr ⟨0, (♯‘𝐴)⟩)) |
40 | 4, 39 | mpdan 686 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr ⟨0, (♯‘𝐴)⟩)) |
41 | | pfxid 14579 |
. . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = 𝐴) |
42 | 40, 41 | eqtr3d 2779 |
. . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨0, (♯‘𝐴)⟩) = 𝐴) |
43 | 38, 42 | eqtrid 2789 |
. . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr ⟨0, 𝐿⟩) = 𝐴) |
44 | 43 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 substr ⟨0, 𝐿⟩) = 𝐴) |
45 | 44 | oveq1d 7377 |
. 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 substr ⟨0, 𝐿⟩) ++ (𝐵 prefix (𝑁 − 𝐿))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |
46 | 14, 36, 45 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |