Proof of Theorem swrdrevpfx
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fznn0sub2 13675 | . . . . . 6
⊢ (𝐹 ∈ (0...𝐿) → (𝐿 − 𝐹) ∈ (0...𝐿)) | 
| 2 |  | pfxcl 14715 | . . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix 𝐿) ∈ Word 𝑉) | 
| 3 |  | revcl 14799 | . . . . . . . . 9
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉) | 
| 4 | 2, 3 | syl 17 | . . . . . . . 8
⊢ (𝑊 ∈ Word 𝑉 → (reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉) | 
| 5 | 4 | 3ad2ant1 1134 | . . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) → (reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉) | 
| 6 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) → (𝐿 − 𝐹) ∈ (0...𝐿)) | 
| 7 |  | revlen 14800 | . . . . . . . . . . . . 13
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) | 
| 8 | 2, 7 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = (♯‘(𝑊 prefix 𝐿))) | 
| 10 |  | pfxlen 14721 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 prefix 𝐿)) = 𝐿) | 
| 11 | 9, 10 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = 𝐿) | 
| 12 | 11 | 3adant3 1133 | . . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = 𝐿) | 
| 13 | 12 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) →
(0...(♯‘(reverse‘(𝑊 prefix 𝐿)))) = (0...𝐿)) | 
| 14 | 6, 13 | eleqtrrd 2844 | . . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) → (𝐿 − 𝐹) ∈
(0...(♯‘(reverse‘(𝑊 prefix 𝐿))))) | 
| 15 | 5, 14 | jca 511 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ (𝐿 − 𝐹) ∈ (0...𝐿)) → ((reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉 ∧ (𝐿 − 𝐹) ∈
(0...(♯‘(reverse‘(𝑊 prefix 𝐿)))))) | 
| 16 | 1, 15 | syl3an3 1166 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐹 ∈ (0...𝐿)) → ((reverse‘(𝑊 prefix 𝐿)) ∈ Word 𝑉 ∧ (𝐿 − 𝐹) ∈
(0...(♯‘(reverse‘(𝑊 prefix 𝐿)))))) | 
| 17 | 16 | 3com23 1127 | . . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((reverse‘(𝑊 prefix
𝐿)) ∈ Word 𝑉 ∧ (𝐿 − 𝐹) ∈
(0...(♯‘(reverse‘(𝑊 prefix 𝐿)))))) | 
| 18 |  | revpfxsfxrev 35121 | . . . 4
⊢
(((reverse‘(𝑊
prefix 𝐿)) ∈ Word
𝑉 ∧ (𝐿 − 𝐹) ∈
(0...(♯‘(reverse‘(𝑊 prefix 𝐿))))) →
(reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))) = ((reverse‘(reverse‘(𝑊 prefix 𝐿))) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉)) | 
| 19 | 17, 18 | syl 17 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))) = ((reverse‘(reverse‘(𝑊 prefix 𝐿))) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉)) | 
| 20 |  | revrev 14805 | . . . . . 6
⊢ ((𝑊 prefix 𝐿) ∈ Word 𝑉 → (reverse‘(reverse‘(𝑊 prefix 𝐿))) = (𝑊 prefix 𝐿)) | 
| 21 | 2, 20 | syl 17 | . . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (reverse‘(reverse‘(𝑊 prefix 𝐿))) = (𝑊 prefix 𝐿)) | 
| 22 | 21 | oveq1d 7446 | . . . 4
⊢ (𝑊 ∈ Word 𝑉 →
((reverse‘(reverse‘(𝑊 prefix 𝐿))) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉) = ((𝑊 prefix 𝐿) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉)) | 
| 23 | 22 | 3ad2ant1 1134 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((reverse‘(reverse‘(𝑊 prefix 𝐿))) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉) = ((𝑊 prefix 𝐿) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉)) | 
| 24 | 11 | oveq1d 7446 | . . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)) = (𝐿 − (𝐿 − 𝐹))) | 
| 25 | 24 | 3adant2 1132 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)) = (𝐿 − (𝐿 − 𝐹))) | 
| 26 |  | elfzel2 13562 | . . . . . . . . 9
⊢ (𝐹 ∈ (0...𝐿) → 𝐿 ∈ ℤ) | 
| 27 | 26 | zcnd 12723 | . . . . . . . 8
⊢ (𝐹 ∈ (0...𝐿) → 𝐿 ∈ ℂ) | 
| 28 |  | elfzelz 13564 | . . . . . . . . 9
⊢ (𝐹 ∈ (0...𝐿) → 𝐹 ∈ ℤ) | 
| 29 | 28 | zcnd 12723 | . . . . . . . 8
⊢ (𝐹 ∈ (0...𝐿) → 𝐹 ∈ ℂ) | 
| 30 | 27, 29 | nncand 11625 | . . . . . . 7
⊢ (𝐹 ∈ (0...𝐿) → (𝐿 − (𝐿 − 𝐹)) = 𝐹) | 
| 31 | 30 | 3ad2ant2 1135 | . . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝐿 − (𝐿 − 𝐹)) = 𝐹) | 
| 32 | 25, 31 | eqtrd 2777 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)) = 𝐹) | 
| 33 | 11 | 3adant2 1132 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(♯‘(reverse‘(𝑊 prefix 𝐿))) = 𝐿) | 
| 34 | 32, 33 | opeq12d 4881 | . . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉 = 〈𝐹, 𝐿〉) | 
| 35 | 34 | oveq2d 7447 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝐿) substr
〈((♯‘(reverse‘(𝑊 prefix 𝐿))) − (𝐿 − 𝐹)), (♯‘(reverse‘(𝑊 prefix 𝐿)))〉) = ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉)) | 
| 36 | 19, 23, 35 | 3eqtrd 2781 | . 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) →
(reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹))) = ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉)) | 
| 37 |  | elfzuz3 13561 | . . . . . . . 8
⊢ (𝐹 ∈ (0...𝐿) → 𝐿 ∈ (ℤ≥‘𝐹)) | 
| 38 |  | eluzfz2 13572 | . . . . . . . 8
⊢ (𝐿 ∈
(ℤ≥‘𝐹) → 𝐿 ∈ (𝐹...𝐿)) | 
| 39 | 37, 38 | syl 17 | . . . . . . 7
⊢ (𝐹 ∈ (0...𝐿) → 𝐿 ∈ (𝐹...𝐿)) | 
| 40 | 39 | ancli 548 | . . . . . 6
⊢ (𝐹 ∈ (0...𝐿) → (𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (𝐹...𝐿))) | 
| 41 | 40 | 3ad2ant2 1135 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (𝐹...𝐿))) | 
| 42 |  | swrdpfx 14745 | . . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (𝐹...𝐿)) → ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉) = (𝑊 substr 〈𝐹, 𝐿〉))) | 
| 43 | 41, 42 | syl5 34 | . . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉) = (𝑊 substr 〈𝐹, 𝐿〉))) | 
| 44 | 43 | 3adant2 1132 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉) = (𝑊 substr 〈𝐹, 𝐿〉))) | 
| 45 | 44 | pm2.43i 52 | . 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ((𝑊 prefix 𝐿) substr 〈𝐹, 𝐿〉) = (𝑊 substr 〈𝐹, 𝐿〉)) | 
| 46 | 36, 45 | eqtr2d 2778 | 1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 substr 〈𝐹, 𝐿〉) =
(reverse‘((reverse‘(𝑊 prefix 𝐿)) prefix (𝐿 − 𝐹)))) |