Proof of Theorem ccats1pfxeq
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . 4
⊢ (𝑊 = (𝑈 prefix (#‘𝑊)) → (𝑊 ++ 〈“( lastS ‘𝑈)”〉) = ((𝑈 prefix (#‘𝑊)) ++ 〈“( lastS
‘𝑈)”〉)) |
2 | 1 | adantl 481 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) ∧ 𝑊 = (𝑈 prefix (#‘𝑊))) → (𝑊 ++ 〈“( lastS ‘𝑈)”〉) = ((𝑈 prefix (#‘𝑊)) ++ 〈“( lastS
‘𝑈)”〉)) |
3 | | lencl 13179 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
4 | 3 | nn0cnd 11230 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈ ℂ) |
5 | | pncan1 10333 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℂ → (((#‘𝑊) + 1) − 1) = (#‘𝑊)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (((#‘𝑊) + 1) − 1) = (#‘𝑊)) |
7 | 6 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) = (((#‘𝑊) + 1) − 1)) |
8 | 7 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (#‘𝑊) = (((#‘𝑊) + 1) − 1)) |
9 | | oveq1 6556 |
. . . . . . . . . 10
⊢
((#‘𝑈) =
((#‘𝑊) + 1) →
((#‘𝑈) − 1) =
(((#‘𝑊) + 1) −
1)) |
10 | 9 | eqcomd 2616 |
. . . . . . . . 9
⊢
((#‘𝑈) =
((#‘𝑊) + 1) →
(((#‘𝑊) + 1) −
1) = ((#‘𝑈) −
1)) |
11 | 10 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (((#‘𝑊) + 1) − 1) = ((#‘𝑈) − 1)) |
12 | 8, 11 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (#‘𝑊) = ((#‘𝑈) − 1)) |
13 | 12 | oveq2d 6565 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑈 prefix (#‘𝑊)) = (𝑈 prefix ((#‘𝑈) − 1))) |
14 | 13 | oveq1d 6564 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → ((𝑈 prefix (#‘𝑊)) ++ 〈“( lastS ‘𝑈)”〉) = ((𝑈 prefix ((#‘𝑈) − 1)) ++ 〈“(
lastS ‘𝑈)”〉)) |
15 | | simp2 1055 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → 𝑈 ∈ Word 𝑉) |
16 | | nn0p1gt0 11199 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → 0 < ((#‘𝑊) + 1)) |
17 | 3, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → 0 < ((#‘𝑊) + 1)) |
18 | 17 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → 0 < ((#‘𝑊) + 1)) |
19 | | breq2 4587 |
. . . . . . . . 9
⊢
((#‘𝑈) =
((#‘𝑊) + 1) → (0
< (#‘𝑈) ↔ 0
< ((#‘𝑊) +
1))) |
20 | 19 | 3ad2ant3 1077 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (0 < (#‘𝑈) ↔ 0 < ((#‘𝑊) + 1))) |
21 | 18, 20 | mpbird 246 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → 0 < (#‘𝑈)) |
22 | | hashneq0 13016 |
. . . . . . . 8
⊢ (𝑈 ∈ Word 𝑉 → (0 < (#‘𝑈) ↔ 𝑈 ≠ ∅)) |
23 | 22 | 3ad2ant2 1076 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (0 < (#‘𝑈) ↔ 𝑈 ≠ ∅)) |
24 | 21, 23 | mpbid 221 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → 𝑈 ≠ ∅) |
25 | | pfxlswccat 40283 |
. . . . . 6
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑈 ≠ ∅) → ((𝑈 prefix ((#‘𝑈) − 1)) ++ 〈“( lastS
‘𝑈)”〉) =
𝑈) |
26 | 15, 24, 25 | syl2anc 691 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → ((𝑈 prefix ((#‘𝑈) − 1)) ++ 〈“( lastS
‘𝑈)”〉) =
𝑈) |
27 | 14, 26 | eqtrd 2644 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → ((𝑈 prefix (#‘𝑊)) ++ 〈“( lastS ‘𝑈)”〉) = 𝑈) |
28 | 27 | adantr 480 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) ∧ 𝑊 = (𝑈 prefix (#‘𝑊))) → ((𝑈 prefix (#‘𝑊)) ++ 〈“( lastS ‘𝑈)”〉) = 𝑈) |
29 | 2, 28 | eqtr2d 2645 |
. 2
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) ∧ 𝑊 = (𝑈 prefix (#‘𝑊))) → 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉)) |
30 | 29 | ex 449 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ (#‘𝑈) = ((#‘𝑊) + 1)) → (𝑊 = (𝑈 prefix (#‘𝑊)) → 𝑈 = (𝑊 ++ 〈“( lastS ‘𝑈)”〉))) |