Proof of Theorem swrdccatwrd
Step | Hyp | Ref
| Expression |
1 | | lennncl 13180 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈
ℕ) |
2 | | fzo0end 12426 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ (0..^(#‘𝑊))) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((#‘𝑊) − 1) ∈
(0..^(#‘𝑊))) |
4 | | swrds1 13303 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ ((#‘𝑊) − 1) ∈ (0..^(#‘𝑊))) → (𝑊 substr 〈((#‘𝑊) − 1), (((#‘𝑊) − 1) + 1)〉) =
〈“(𝑊‘((#‘𝑊) − 1))”〉) |
5 | 3, 4 | syldan 486 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((#‘𝑊) − 1), (((#‘𝑊) − 1) + 1)〉) =
〈“(𝑊‘((#‘𝑊) − 1))”〉) |
6 | | nncn 10905 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℂ) |
7 | | 1cnd 9935 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ → 1 ∈ ℂ) |
8 | 6, 7 | npcand 10275 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℕ → (((#‘𝑊) − 1) + 1) = (#‘𝑊)) |
9 | 8 | eqcomd 2616 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
= (((#‘𝑊) − 1)
+ 1)) |
10 | 1, 9 | syl 17 |
. . . . . 6
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (#‘𝑊) = (((#‘𝑊) − 1) + 1)) |
11 | 10 | opeq2d 4347 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 〈((#‘𝑊) − 1), (#‘𝑊)〉 = 〈((#‘𝑊) − 1), (((#‘𝑊) − 1) +
1)〉) |
12 | 11 | oveq2d 6565 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉) = (𝑊 substr 〈((#‘𝑊) − 1), (((#‘𝑊) − 1) + 1)〉)) |
13 | | lsw 13204 |
. . . . . 6
⊢ (𝑊 ∈ Word 𝑉 → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
14 | 13 | adantr 480 |
. . . . 5
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ( lastS ‘𝑊) = (𝑊‘((#‘𝑊) − 1))) |
15 | 14 | s1eqd 13234 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 〈“( lastS
‘𝑊)”〉 =
〈“(𝑊‘((#‘𝑊) − 1))”〉) |
16 | 5, 12, 15 | 3eqtr4rd 2655 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → 〈“( lastS
‘𝑊)”〉 =
(𝑊 substr
〈((#‘𝑊) −
1), (#‘𝑊)〉)) |
17 | 16 | oveq2d 6565 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ++ 〈“( lastS
‘𝑊)”〉) =
((𝑊 substr 〈0,
((#‘𝑊) −
1)〉) ++ (𝑊 substr
〈((#‘𝑊) −
1), (#‘𝑊)〉))) |
18 | | nnm1nn0 11211 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ ℕ0) |
19 | | 0elfz 12305 |
. . . . . 6
⊢
(((#‘𝑊)
− 1) ∈ ℕ0 → 0 ∈ (0...((#‘𝑊) − 1))) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢
((#‘𝑊) ∈
ℕ → 0 ∈ (0...((#‘𝑊) − 1))) |
21 | | 1nn0 11185 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
22 | 21 | a1i 11 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ → 1 ∈ ℕ0) |
23 | | nnnn0 11176 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ ℕ0) |
24 | | nnge1 10923 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ → 1 ≤ (#‘𝑊)) |
25 | | elfz2nn0 12300 |
. . . . . . 7
⊢ (1 ∈
(0...(#‘𝑊)) ↔ (1
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0 ∧ 1 ≤
(#‘𝑊))) |
26 | 22, 23, 24, 25 | syl3anbrc 1239 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ → 1 ∈ (0...(#‘𝑊))) |
27 | | elfz1end 12242 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ ↔ (#‘𝑊)
∈ (1...(#‘𝑊))) |
28 | 27 | biimpi 205 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ (1...(#‘𝑊))) |
29 | | fz0fzdiffz0 12317 |
. . . . . 6
⊢ ((1
∈ (0...(#‘𝑊))
∧ (#‘𝑊) ∈
(1...(#‘𝑊))) →
((#‘𝑊) − 1)
∈ (0...(#‘𝑊))) |
30 | 26, 28, 29 | syl2anc 691 |
. . . . 5
⊢
((#‘𝑊) ∈
ℕ → ((#‘𝑊)
− 1) ∈ (0...(#‘𝑊))) |
31 | | nn0fz0 12306 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ0 ↔ (#‘𝑊) ∈ (0...(#‘𝑊))) |
32 | 31 | biimpi 205 |
. . . . . 6
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ (0...(#‘𝑊))) |
33 | 23, 32 | syl 17 |
. . . . 5
⊢
((#‘𝑊) ∈
ℕ → (#‘𝑊)
∈ (0...(#‘𝑊))) |
34 | 20, 30, 33 | 3jca 1235 |
. . . 4
⊢
((#‘𝑊) ∈
ℕ → (0 ∈ (0...((#‘𝑊) − 1)) ∧ ((#‘𝑊) − 1) ∈
(0...(#‘𝑊)) ∧
(#‘𝑊) ∈
(0...(#‘𝑊)))) |
35 | 1, 34 | syl 17 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (0 ∈
(0...((#‘𝑊) −
1)) ∧ ((#‘𝑊)
− 1) ∈ (0...(#‘𝑊)) ∧ (#‘𝑊) ∈ (0...(#‘𝑊)))) |
36 | | ccatswrd 13308 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (0 ∈ (0...((#‘𝑊) − 1)) ∧
((#‘𝑊) − 1)
∈ (0...(#‘𝑊))
∧ (#‘𝑊) ∈
(0...(#‘𝑊)))) →
((𝑊 substr 〈0,
((#‘𝑊) −
1)〉) ++ (𝑊 substr
〈((#‘𝑊) −
1), (#‘𝑊)〉)) =
(𝑊 substr 〈0,
(#‘𝑊)〉)) |
37 | 35, 36 | syldan 486 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ++ (𝑊 substr 〈((#‘𝑊) − 1), (#‘𝑊)〉)) = (𝑊 substr 〈0, (#‘𝑊)〉)) |
38 | | swrdid 13280 |
. . 3
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 substr 〈0, (#‘𝑊)〉) = 𝑊) |
39 | 38 | adantr 480 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr 〈0, (#‘𝑊)〉) = 𝑊) |
40 | 17, 37, 39 | 3eqtrd 2648 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ++ 〈“( lastS
‘𝑊)”〉) =
𝑊) |