Proof of Theorem pfxsuff1eqwrdeq
Step | Hyp | Ref
| Expression |
1 | | hashgt0n0 13156 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → 𝑊 ≠ ∅) |
2 | | lennncl 13325 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
3 | 1, 2 | syldan 487 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
4 | 3 | 3adant2 1080 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
5 | | fzo0end 12560 |
. . . 4
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ (0..^(#‘𝑊))) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) |
7 | | pfxsuffeqwrdeq 41406 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))))) |
8 | 6, 7 | syld3an3 1371 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))))) |
9 | | hashneq0 13155 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) ↔ 𝑊 ≠ ∅)) |
10 | 9 | biimpd 219 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (0 < (#‘𝑊) → 𝑊 ≠ ∅)) |
11 | 10 | imdistani 726 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
12 | 11 | 3adant2 1080 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
13 | 12 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅)) |
14 | | swrdlsw 13452 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑊)”〉) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑊)”〉) |
16 | | breq2 4657 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) → (0 <
(#‘𝑊) ↔ 0 <
(#‘𝑈))) |
17 | 16 | 3anbi3d 1405 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)))) |
18 | | hashneq0 13155 |
. . . . . . . . . . . . 13
⊢ (𝑈 ∈ Word 𝑉 → (0 < (#‘𝑈) ↔ 𝑈 ≠ ∅)) |
19 | 18 | biimpd 219 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ Word 𝑉 → (0 < (#‘𝑈) → 𝑈 ≠ ∅)) |
20 | 19 | imdistani 726 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅)) |
21 | 20 | 3adant1 1079 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅)) |
22 | | swrdlsw 13452 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
24 | 17, 23 | syl6bi 243 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉)) |
25 | 24 | impcom 446 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS ‘𝑈)”〉) |
26 | | oveq1 6657 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) →
((#‘𝑊) − 1) =
((#‘𝑈) −
1)) |
27 | | id 22 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) →
(#‘𝑊) =
(#‘𝑈)) |
28 | 26, 27 | opeq12d 4410 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) →
〈((#‘𝑊) −
1), (#‘𝑊)〉 =
〈((#‘𝑈) −
1), (#‘𝑈)〉) |
29 | 28 | oveq2d 6666 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉)) |
30 | 29 | eqeq1d 2624 |
. . . . . . . 8
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS
‘𝑈)”〉
↔ (𝑈 substr
〈((#‘𝑈) −
1), (#‘𝑈)〉) =
〈“( lastS ‘𝑈)”〉)) |
31 | 30 | adantl 482 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑈)”〉 ↔ (𝑈 substr 〈((#‘𝑈) − 1), (#‘𝑈)〉) = 〈“( lastS
‘𝑈)”〉)) |
32 | 25, 31 | mpbird 247 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = 〈“( lastS ‘𝑈)”〉) |
33 | 15, 32 | eqeq12d 2637 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) ↔ 〈“( lastS
‘𝑊)”〉 =
〈“( lastS ‘𝑈)”〉)) |
34 | | fvexd 6203 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ( lastS ‘𝑊) ∈ V) |
35 | | fvex 6201 |
. . . . . 6
⊢ ( lastS
‘𝑈) ∈
V |
36 | | s111 13395 |
. . . . . 6
⊢ ((( lastS
‘𝑊) ∈ V ∧ (
lastS ‘𝑈) ∈ V)
→ (〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉
↔ ( lastS ‘𝑊) =
( lastS ‘𝑈))) |
37 | 34, 35, 36 | sylancl 694 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“( lastS ‘𝑊)”〉 = 〈“(
lastS ‘𝑈)”〉 ↔ ( lastS ‘𝑊) = ( lastS ‘𝑈))) |
38 | 33, 37 | bitrd 268 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) ↔ ( lastS ‘𝑊) = ( lastS ‘𝑈))) |
39 | 38 | anbi2d 740 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉)) ↔ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))) |
40 | 39 | pm5.32da 673 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉))) ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |
41 | 8, 40 | bitrd 268 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 prefix ((#‘𝑊) − 1)) = (𝑈 prefix ((#‘𝑊) − 1)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |