Proof of Theorem pfxlsw2ccat
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 ∈ Word 𝑉) |
2 | | simpr 488 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 2 ≤ 𝑁) |
3 | | pfxlsw2ccat.n |
. . . . . 6
⊢ 𝑁 = (♯‘𝑊) |
4 | 2, 3 | breqtrdi 5094 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 2 ≤ (♯‘𝑊)) |
5 | | wrdlenge2n0 14107 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 𝑊 ≠ ∅) |
6 | 1, 4, 5 | syl2anc 587 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 ≠ ∅) |
7 | | pfxlswccat 14278 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 prefix ((♯‘𝑊) − 1)) ++
〈“(lastS‘𝑊)”〉) = 𝑊) |
8 | 1, 6, 7 | syl2anc 587 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑊 prefix ((♯‘𝑊) − 1)) ++
〈“(lastS‘𝑊)”〉) = 𝑊) |
9 | | lsw 14119 |
. . . . . . 7
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1))) |
10 | 3 | oveq1i 7223 |
. . . . . . . 8
⊢ (𝑁 − 1) =
((♯‘𝑊) −
1) |
11 | 10 | fveq2i 6720 |
. . . . . . 7
⊢ (𝑊‘(𝑁 − 1)) = (𝑊‘((♯‘𝑊) − 1)) |
12 | 9, 11 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘𝑊) = (𝑊‘(𝑁 − 1))) |
13 | 1, 12 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (lastS‘𝑊) = (𝑊‘(𝑁 − 1))) |
14 | 13 | s1eqd 14158 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 〈“(lastS‘𝑊)”〉 =
〈“(𝑊‘(𝑁 − 1))”〉) |
15 | 14 | oveq2d 7229 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑊 prefix ((♯‘𝑊) − 1)) ++
〈“(lastS‘𝑊)”〉) = ((𝑊 prefix ((♯‘𝑊) − 1)) ++ 〈“(𝑊‘(𝑁 − 1))”〉)) |
16 | 8, 15 | eqtr3d 2779 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 = ((𝑊 prefix ((♯‘𝑊) − 1)) ++ 〈“(𝑊‘(𝑁 − 1))”〉)) |
17 | | pfxcl 14242 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix ((♯‘𝑊) − 1)) ∈ Word 𝑉) |
18 | 1, 17 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊 prefix ((♯‘𝑊) − 1)) ∈ Word 𝑉) |
19 | | lencl 14088 |
. . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
20 | 1, 19 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (♯‘𝑊) ∈
ℕ0) |
21 | 3, 20 | eqeltrid 2842 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑁 ∈
ℕ0) |
22 | | nn0ge2m1nn 12159 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 2 ≤ 𝑁) →
(𝑁 − 1) ∈
ℕ) |
23 | 21, 2, 22 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈ ℕ) |
24 | 10, 23 | eqeltrrid 2843 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ∈
ℕ) |
25 | 20 | nn0red 12151 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (♯‘𝑊) ∈ ℝ) |
26 | 25 | lem1d 11765 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ≤ (♯‘𝑊)) |
27 | | pfxn0 14251 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈ ℕ ∧
((♯‘𝑊) −
1) ≤ (♯‘𝑊))
→ (𝑊 prefix
((♯‘𝑊) −
1)) ≠ ∅) |
28 | 1, 24, 26, 27 | syl3anc 1373 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊 prefix ((♯‘𝑊) − 1)) ≠ ∅) |
29 | | pfxlswccat 14278 |
. . . . 5
⊢ (((𝑊 prefix ((♯‘𝑊) − 1)) ∈ Word 𝑉 ∧ (𝑊 prefix ((♯‘𝑊) − 1)) ≠ ∅) → (((𝑊 prefix ((♯‘𝑊) − 1)) prefix
((♯‘(𝑊 prefix
((♯‘𝑊) −
1))) − 1)) ++ 〈“(lastS‘(𝑊 prefix ((♯‘𝑊) − 1)))”〉) = (𝑊 prefix ((♯‘𝑊) − 1))) |
30 | 18, 28, 29 | syl2anc 587 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((𝑊 prefix ((♯‘𝑊) − 1)) prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) ++
〈“(lastS‘(𝑊 prefix ((♯‘𝑊) − 1)))”〉) = (𝑊 prefix ((♯‘𝑊) − 1))) |
31 | | ige2m1fz 13202 |
. . . . . . . 8
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 2 ≤ (♯‘𝑊)) → ((♯‘𝑊) − 1) ∈
(0...(♯‘𝑊))) |
32 | 20, 4, 31 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ∈
(0...(♯‘𝑊))) |
33 | | pfxlen 14248 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
(0...(♯‘𝑊)))
→ (♯‘(𝑊
prefix ((♯‘𝑊)
− 1))) = ((♯‘𝑊) − 1)) |
34 | 1, 32, 33 | syl2anc 587 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (♯‘(𝑊 prefix ((♯‘𝑊) − 1))) = ((♯‘𝑊) − 1)) |
35 | 34 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1) =
(((♯‘𝑊) −
1) − 1)) |
36 | | 0zd 12188 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 0 ∈ ℤ) |
37 | | nn0ge2m1nn0 12160 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℕ0
∧ 2 ≤ 𝑁) →
(𝑁 − 1) ∈
ℕ0) |
38 | 21, 2, 37 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑁 − 1) ∈
ℕ0) |
39 | 10, 38 | eqeltrrid 2843 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ∈
ℕ0) |
40 | 39 | nn0zd 12280 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ∈
ℤ) |
41 | | 1zzd 12208 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 1 ∈ ℤ) |
42 | 40, 41 | zsubcld 12287 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((♯‘𝑊) − 1) − 1) ∈
ℤ) |
43 | | 2nn0 12107 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℕ0 |
44 | 43 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 2 ∈
ℕ0) |
45 | | nn0sub 12140 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (2 ≤
𝑁 ↔ (𝑁 − 2) ∈
ℕ0)) |
46 | 45 | biimpa 480 |
. . . . . . . . . . . . 13
⊢ (((2
∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 2 ≤
𝑁) → (𝑁 − 2) ∈
ℕ0) |
47 | 44, 21, 2, 46 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑁 − 2) ∈
ℕ0) |
48 | 47 | nn0ge0d 12153 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 0 ≤ (𝑁 − 2)) |
49 | 21 | nn0cnd 12152 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑁 ∈ ℂ) |
50 | | sub1m1 12082 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑁 − 1) − 1) = (𝑁 − 2)) |
52 | 48, 51 | breqtrrd 5081 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 0 ≤ ((𝑁 − 1) − 1)) |
53 | 10 | oveq1i 7223 |
. . . . . . . . . 10
⊢ ((𝑁 − 1) − 1) =
(((♯‘𝑊) −
1) − 1) |
54 | 52, 53 | breqtrdi 5094 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 0 ≤ (((♯‘𝑊) − 1) −
1)) |
55 | 24 | nnred 11845 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘𝑊) − 1) ∈
ℝ) |
56 | 55 | lem1d 11765 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((♯‘𝑊) − 1) − 1) ≤
((♯‘𝑊) −
1)) |
57 | 36, 40, 42, 54, 56 | elfzd 13103 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((♯‘𝑊) − 1) − 1) ∈
(0...((♯‘𝑊)
− 1))) |
58 | 35, 57 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1) ∈
(0...((♯‘𝑊)
− 1))) |
59 | | pfxpfx 14273 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 1) ∈
(0...(♯‘𝑊))
∧ ((♯‘(𝑊
prefix ((♯‘𝑊)
− 1))) − 1) ∈ (0...((♯‘𝑊) − 1))) → ((𝑊 prefix ((♯‘𝑊) − 1)) prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) =
(𝑊 prefix
((♯‘(𝑊 prefix
((♯‘𝑊) −
1))) − 1))) |
60 | 1, 32, 58, 59 | syl3anc 1373 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑊 prefix ((♯‘𝑊) − 1)) prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) =
(𝑊 prefix
((♯‘(𝑊 prefix
((♯‘𝑊) −
1))) − 1))) |
61 | 34, 10 | eqtr4di 2796 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (♯‘(𝑊 prefix ((♯‘𝑊) − 1))) = (𝑁 − 1)) |
62 | 61 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1) = ((𝑁 − 1) −
1)) |
63 | 62, 51 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1) = (𝑁 − 2)) |
64 | 63 | oveq2d 7229 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊 prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) = (𝑊 prefix (𝑁 − 2))) |
65 | 60, 64 | eqtrd 2777 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑊 prefix ((♯‘𝑊) − 1)) prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) =
(𝑊 prefix (𝑁 − 2))) |
66 | | pfxtrcfvl 14262 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → (lastS‘(𝑊 prefix ((♯‘𝑊) − 1))) = (𝑊‘((♯‘𝑊) − 2))) |
67 | 1, 4, 66 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (lastS‘(𝑊 prefix ((♯‘𝑊) − 1))) = (𝑊‘((♯‘𝑊) − 2))) |
68 | 3 | a1i 11 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑁 = (♯‘𝑊)) |
69 | 68 | fvoveq1d 7235 |
. . . . . . 7
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊‘(𝑁 − 2)) = (𝑊‘((♯‘𝑊) − 2))) |
70 | 67, 69 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (lastS‘(𝑊 prefix ((♯‘𝑊) − 1))) = (𝑊‘(𝑁 − 2))) |
71 | 70 | s1eqd 14158 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 〈“(lastS‘(𝑊 prefix ((♯‘𝑊) − 1)))”〉 =
〈“(𝑊‘(𝑁 − 2))”〉) |
72 | 65, 71 | oveq12d 7231 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((𝑊 prefix ((♯‘𝑊) − 1)) prefix ((♯‘(𝑊 prefix ((♯‘𝑊) − 1))) − 1)) ++
〈“(lastS‘(𝑊 prefix ((♯‘𝑊) − 1)))”〉) = ((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))”〉)) |
73 | 30, 72 | eqtr3d 2779 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊 prefix ((♯‘𝑊) − 1)) = ((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))”〉)) |
74 | 73 | oveq1d 7228 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → ((𝑊 prefix ((♯‘𝑊) − 1)) ++ 〈“(𝑊‘(𝑁 − 1))”〉) = (((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))”〉) ++
〈“(𝑊‘(𝑁 − 1))”〉)) |
75 | | pfxcl 14242 |
. . . 4
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 prefix (𝑁 − 2)) ∈ Word 𝑉) |
76 | 1, 75 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (𝑊 prefix (𝑁 − 2)) ∈ Word 𝑉) |
77 | | ccatw2s1ccatws2 14519 |
. . 3
⊢ ((𝑊 prefix (𝑁 − 2)) ∈ Word 𝑉 → (((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))”〉) ++
〈“(𝑊‘(𝑁 − 1))”〉) = ((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉)) |
78 | 76, 77 | syl 17 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → (((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))”〉) ++
〈“(𝑊‘(𝑁 − 1))”〉) = ((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉)) |
79 | 16, 74, 78 | 3eqtrd 2781 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ 𝑁) → 𝑊 = ((𝑊 prefix (𝑁 − 2)) ++ 〈“(𝑊‘(𝑁 − 2))(𝑊‘(𝑁 − 1))”〉)) |