Proof of Theorem pfxccatpfx2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ccatcl 14613 | . . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) ∈ Word 𝑉) | 
| 2 | 1 | 3adant3 1132 | . . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ++ 𝐵) ∈ Word 𝑉) | 
| 3 |  | swrdccatin2.l | . . . . . . 7
⊢ 𝐿 = (♯‘𝐴) | 
| 4 |  | lencl 14572 | . . . . . . 7
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈
ℕ0) | 
| 5 | 3, 4 | eqeltrid 2844 | . . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈
ℕ0) | 
| 6 |  | elfzuz 13561 | . . . . . 6
⊢ (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (ℤ≥‘(𝐿 + 1))) | 
| 7 |  | peano2nn0 12568 | . . . . . . 7
⊢ (𝐿 ∈ ℕ0
→ (𝐿 + 1) ∈
ℕ0) | 
| 8 | 7 | anim1i 615 | . . . . . 6
⊢ ((𝐿 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) | 
| 9 | 5, 6, 8 | syl2an 596 | . . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) | 
| 10 | 9 | 3adant2 1131 | . . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐿 + 1) ∈ ℕ0 ∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1)))) | 
| 11 |  | eluznn0 12960 | . . . 4
⊢ (((𝐿 + 1) ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘(𝐿 + 1))) → 𝑁 ∈
ℕ0) | 
| 12 | 10, 11 | syl 17 | . . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈
ℕ0) | 
| 13 |  | pfxval 14712 | . . 3
⊢ (((𝐴 ++ 𝐵) ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) | 
| 14 | 2, 12, 13 | syl2anc 584 | . 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = ((𝐴 ++ 𝐵) substr 〈0, 𝑁〉)) | 
| 15 |  | 3simpa 1148 | . . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉)) | 
| 16 | 5 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝐿 ∈
ℕ0) | 
| 17 |  | 0elfz 13665 | . . . . 5
⊢ (𝐿 ∈ ℕ0
→ 0 ∈ (0...𝐿)) | 
| 18 | 16, 17 | syl 17 | . . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 0 ∈ (0...𝐿)) | 
| 19 | 4 | nn0zd 12641 | . . . . . . . . . 10
⊢ (𝐴 ∈ Word 𝑉 → (♯‘𝐴) ∈ ℤ) | 
| 20 | 3, 19 | eqeltrid 2844 | . . . . . . . . 9
⊢ (𝐴 ∈ Word 𝑉 → 𝐿 ∈ ℤ) | 
| 21 | 20 | adantr 480 | . . . . . . . 8
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → 𝐿 ∈ ℤ) | 
| 22 |  | uzid 12894 | . . . . . . . 8
⊢ (𝐿 ∈ ℤ → 𝐿 ∈
(ℤ≥‘𝐿)) | 
| 23 |  | peano2uz 12944 | . . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐿) → (𝐿 + 1) ∈
(ℤ≥‘𝐿)) | 
| 24 |  | fzss1 13604 | . . . . . . . 8
⊢ ((𝐿 + 1) ∈
(ℤ≥‘𝐿) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) | 
| 25 | 21, 22, 23, 24 | 4syl 19 | . . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + 𝑀))) | 
| 26 |  | pfxccatpfx2.m | . . . . . . . . . 10
⊢ 𝑀 = (♯‘𝐵) | 
| 27 | 26 | eqcomi 2745 | . . . . . . . . 9
⊢
(♯‘𝐵) =
𝑀 | 
| 28 | 27 | oveq2i 7443 | . . . . . . . 8
⊢ (𝐿 + (♯‘𝐵)) = (𝐿 + 𝑀) | 
| 29 | 28 | oveq2i 7443 | . . . . . . 7
⊢ (𝐿...(𝐿 + (♯‘𝐵))) = (𝐿...(𝐿 + 𝑀)) | 
| 30 | 25, 29 | sseqtrrdi 4024 | . . . . . 6
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → ((𝐿 + 1)...(𝐿 + 𝑀)) ⊆ (𝐿...(𝐿 + (♯‘𝐵)))) | 
| 31 | 30 | sseld 3981 | . . . . 5
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀)) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) | 
| 32 | 31 | 3impia 1117 | . . . 4
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵)))) | 
| 33 | 18, 32 | jca 511 | . . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (0 ∈ (0...𝐿) ∧ 𝑁 ∈ (𝐿...(𝐿 + (♯‘𝐵))))) | 
| 34 | 3 | pfxccatin12 14772 | . . 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 4876 | . . . . . 6
⊢ 〈0,
𝐿〉 = 〈0,
(♯‘𝐴)〉 | 
| 37 | 36 | oveq2i 7443 | . . . . 5
⊢ (𝐴 substr 〈0, 𝐿〉) = (𝐴 substr 〈0, (♯‘𝐴)〉) | 
| 38 |  | pfxval 14712 | . . . . . . 7
⊢ ((𝐴 ∈ Word 𝑉 ∧ (♯‘𝐴) ∈ ℕ0) → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) | 
| 39 | 4, 38 | mpdan 687 | . . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = (𝐴 substr 〈0, (♯‘𝐴)〉)) | 
| 40 |  | pfxid 14723 | . . . . . 6
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 prefix (♯‘𝐴)) = 𝐴) | 
| 41 | 39, 40 | eqtr3d 2778 | . . . . 5
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, (♯‘𝐴)〉) = 𝐴) | 
| 42 | 37, 41 | eqtrid 2788 | . . . 4
⊢ (𝐴 ∈ Word 𝑉 → (𝐴 substr 〈0, 𝐿〉) = 𝐴) | 
| 43 | 42 | 3ad2ant1 1133 | . . 3
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → (𝐴 substr 〈0, 𝐿〉) = 𝐴) | 
| 44 | 43 | oveq1d 7447 | . 2
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 substr 〈0, 𝐿〉) ++ (𝐵 prefix (𝑁 − 𝐿))) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) | 
| 45 | 14, 35, 44 | 3eqtrd 2780 | 1
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝑁 ∈ ((𝐿 + 1)...(𝐿 + 𝑀))) → ((𝐴 ++ 𝐵) prefix 𝑁) = (𝐴 ++ (𝐵 prefix (𝑁 − 𝐿)))) |