Proof of Theorem pfxsuff1eqwrdeq
Step | Hyp | Ref
| Expression |
1 | | hashgt0n0 13017 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → 𝑊 ≠ ∅) |
2 | | lennncl 13180 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
3 | 1, 2 | syldan 486 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
4 | 3 | 3adant2 1073 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
5 | | fzo0end 12426 |
. . . 4
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ (0..^(#‘𝑊))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) |
7 | | pfxsuffeqwrdeq 40269 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))))) |
8 | 6, 7 | syld3an3 1363 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))))) |
9 | | hashneq0 13016 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
10 | 9 | biimpd 218 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) → 𝑊 ≠ ∅)) |
11 | 10 | imdistani 722 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
12 | 11 | 3adant2 1073 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
13 | 12 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
14 | | swrdlsw 13304 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑊)”〉) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑊)”〉) |
16 | | breq2 4587 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) → (0 <
(#‘𝑊) ↔ 0 <
(#‘𝑈))) |
17 | 16 | 3anbi3d 1397 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)))) |
18 | | hashneq0 13016 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ Word 𝑉 → (0 < (#‘𝑈) ↔ 𝑈 ≠ ∅)) |
19 | 18 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Word 𝑉 → (0 < (#‘𝑈) → 𝑈 ≠ ∅)) |
20 | 19 | imdistani 722 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅)) |
21 | 20 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅)) |
22 | | swrdlsw 13304 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
24 | 17, 23 | syl6bi 242 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉)) |
25 | 24 | impcom 445 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
26 | | oveq1 6556 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) →
((#‘𝑊) − 1) =
((#‘𝑈) −
1)) |
27 | | id 22 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) →
(#‘𝑊) =
(#‘𝑈)) |
28 | 26, 27 | opeq12d 4348 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) →
〈((#‘𝑊) −
1), (#‘𝑊)〉 =
〈((#‘𝑈) −
1), (#‘𝑈)〉) |
29 | 28 | oveq2d 6565 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS
‘𝑈)”〉
↔ (𝑈 substr
〈((#‘𝑈) −
1), (#‘𝑈)〉) =
〈“( lastS ‘𝑈)”〉)) |
31 | 30 | adantl 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑈)”〉 ↔ (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS
‘𝑈)”〉)) |
32 | 25, 31 | mpbird 246 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑈)”〉) |
33 | 15, 32 | eqeq12d 2625 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) ↔ 〈“( lastS
‘𝑊)”〉 =
〈“( lastS ‘𝑈)”〉)) |
34 | | fvex 6113 |
. . . . . . 7
⊢ ( lastS
‘𝑊) ∈
V |
35 | 34 | a1i 11 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ( lastS ‘𝑊) ∈ V) |
36 | | fvex 6113 |
. . . . . 6
⊢ ( lastS
‘𝑈) ∈
V |
37 | | s111 13248 |
. . . . . 6
⊢ ((( lastS
‘𝑊) ∈ V ∧ (
lastS ‘𝑈) ∈ V)
→ (〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉
↔ ( lastS ‘𝑊) =
( lastS ‘𝑈))) |
38 | 35, 36, 37 | sylancl 693 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“( lastS ‘𝑊)”〉 = 〈“(
lastS ‘𝑈)”〉 ↔ ( lastS ‘𝑊) = ( lastS ‘𝑈))) |
39 | 33, 38 | bitrd 267 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) ↔ ( lastS ‘𝑊) = ( lastS ‘𝑈))) |
40 | 39 | anbi2d 736 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉)) ↔ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))) |
41 | 40 | pm5.32da 671 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))) ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |
42 | 8, 41 | bitrd 267 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |