Proof of Theorem 2swrd2eqwrdeq
Step | Hyp | Ref
| Expression |
1 | | lencl 13179 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∈
ℕ0) |
2 | | 1z 11284 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
3 | | nn0z 11277 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℤ) |
4 | | zltp1le 11304 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ (#‘𝑊) ∈ ℤ) → (1 <
(#‘𝑊) ↔ (1 + 1)
≤ (#‘𝑊))) |
5 | 2, 3, 4 | sylancr 694 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ0 → (1 < (#‘𝑊) ↔ (1 + 1) ≤ (#‘𝑊))) |
6 | | 1p1e2 11011 |
. . . . . . . . . . . 12
⊢ (1 + 1) =
2 |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((#‘𝑊) ∈
ℕ0 → (1 + 1) = 2) |
8 | 7 | breq1d 4593 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → ((1 + 1) ≤ (#‘𝑊) ↔ 2 ≤ (#‘𝑊))) |
9 | 8 | biimpd 218 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ0 → ((1 + 1) ≤ (#‘𝑊) → 2 ≤ (#‘𝑊))) |
10 | 5, 9 | sylbid 229 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℕ0 → (1 < (#‘𝑊) → 2 ≤ (#‘𝑊))) |
11 | 10 | imp 444 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → 2 ≤ (#‘𝑊)) |
12 | | 2nn0 11186 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
13 | | simpl 472 |
. . . . . . . 8
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → (#‘𝑊) ∈
ℕ0) |
14 | | nn0sub 11220 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ (#‘𝑊) ∈ ℕ0) → (2 ≤
(#‘𝑊) ↔
((#‘𝑊) − 2)
∈ ℕ0)) |
15 | 12, 13, 14 | sylancr 694 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → (2 ≤ (#‘𝑊) ↔ ((#‘𝑊) − 2) ∈
ℕ0)) |
16 | 11, 15 | mpbid 221 |
. . . . . 6
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → ((#‘𝑊) − 2) ∈
ℕ0) |
17 | 3 | adantr 480 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → (#‘𝑊) ∈ ℤ) |
18 | | 0red 9920 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → 0 ∈ ℝ) |
19 | | 1red 9934 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → 1 ∈ ℝ) |
20 | | nn0re 11178 |
. . . . . . . . . 10
⊢
((#‘𝑊) ∈
ℕ0 → (#‘𝑊) ∈ ℝ) |
21 | 18, 19, 20 | 3jca 1235 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ0 → (0 ∈ ℝ ∧ 1 ∈ ℝ ∧
(#‘𝑊) ∈
ℝ)) |
22 | | 0lt1 10429 |
. . . . . . . . 9
⊢ 0 <
1 |
23 | | lttr 9993 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → ((0 < 1 ∧ 1
< (#‘𝑊)) → 0
< (#‘𝑊))) |
24 | 23 | expd 451 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (#‘𝑊) ∈ ℝ) → (0 < 1 → (1
< (#‘𝑊) → 0
< (#‘𝑊)))) |
25 | 21, 22, 24 | mpisyl 21 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℕ0 → (1 < (#‘𝑊) → 0 < (#‘𝑊))) |
26 | 25 | imp 444 |
. . . . . . 7
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → 0 < (#‘𝑊)) |
27 | | elnnz 11264 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ ↔ ((#‘𝑊)
∈ ℤ ∧ 0 < (#‘𝑊))) |
28 | 17, 26, 27 | sylanbrc 695 |
. . . . . 6
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → (#‘𝑊) ∈ ℕ) |
29 | | 2pos 10989 |
. . . . . . . 8
⊢ 0 <
2 |
30 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢
((#‘𝑊) ∈
ℕ0 → 2 ∈ ℝ) |
32 | 31, 20 | ltsubposd 10492 |
. . . . . . . 8
⊢
((#‘𝑊) ∈
ℕ0 → (0 < 2 ↔ ((#‘𝑊) − 2) < (#‘𝑊))) |
33 | 29, 32 | mpbii 222 |
. . . . . . 7
⊢
((#‘𝑊) ∈
ℕ0 → ((#‘𝑊) − 2) < (#‘𝑊)) |
34 | 33 | adantr 480 |
. . . . . 6
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → ((#‘𝑊) − 2) < (#‘𝑊)) |
35 | | elfzo0 12376 |
. . . . . 6
⊢
(((#‘𝑊)
− 2) ∈ (0..^(#‘𝑊)) ↔ (((#‘𝑊) − 2) ∈ ℕ0
∧ (#‘𝑊) ∈
ℕ ∧ ((#‘𝑊)
− 2) < (#‘𝑊))) |
36 | 16, 28, 34, 35 | syl3anbrc 1239 |
. . . . 5
⊢
(((#‘𝑊) ∈
ℕ0 ∧ 1 < (#‘𝑊)) → ((#‘𝑊) − 2) ∈ (0..^(#‘𝑊))) |
37 | 1, 36 | sylan 487 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → ((#‘𝑊) − 2) ∈ (0..^(#‘𝑊))) |
38 | 37 | 3adant2 1073 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → ((#‘𝑊) − 2) ∈ (0..^(#‘𝑊))) |
39 | | 2swrdeqwrdeq 13305 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ((#‘𝑊) − 2) ∈ (0..^(#‘𝑊))) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉))))) |
40 | 38, 39 | syld3an3 1363 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉))))) |
41 | | swrd2lsw 13543 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉) |
42 | 41 | 3adant2 1073 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉) |
43 | 42 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉) |
44 | | breq2 4587 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) → (1 <
(#‘𝑊) ↔ 1 <
(#‘𝑈))) |
45 | 44 | 3anbi3d 1397 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑈)))) |
46 | | swrd2lsw 13543 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉) |
47 | 46 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉) |
48 | 45, 47 | syl6bi 242 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉)) |
49 | 48 | impcom 445 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉) |
50 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) =
(#‘𝑈) →
((#‘𝑊) − 2) =
((#‘𝑈) −
2)) |
51 | | id 22 |
. . . . . . . . . . . 12
⊢
((#‘𝑊) =
(#‘𝑈) →
(#‘𝑊) =
(#‘𝑈)) |
52 | 50, 51 | opeq12d 4348 |
. . . . . . . . . . 11
⊢
((#‘𝑊) =
(#‘𝑈) →
〈((#‘𝑊) −
2), (#‘𝑊)〉 =
〈((#‘𝑈) −
2), (#‘𝑈)〉) |
53 | 52 | oveq2d 6565 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) → (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉)) |
54 | 53 | eqeq1d 2612 |
. . . . . . . . 9
⊢
((#‘𝑊) =
(#‘𝑈) → ((𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS
‘𝑈)”〉
↔ (𝑈 substr
〈((#‘𝑈) −
2), (#‘𝑈)〉) =
〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉)) |
55 | 54 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉 ↔ (𝑈 substr 〈((#‘𝑈) − 2), (#‘𝑈)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS
‘𝑈)”〉)) |
56 | 49, 55 | mpbird 246 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = 〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉) |
57 | 43, 56 | eqeq12d 2625 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) ↔ 〈“(𝑊‘((#‘𝑊) − 2))( lastS
‘𝑊)”〉 =
〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉)) |
58 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑊‘((#‘𝑊) − 2)) ∈
V |
59 | 58 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑊‘((#‘𝑊) − 2)) ∈ V) |
60 | | fvex 6113 |
. . . . . . . 8
⊢ ( lastS
‘𝑊) ∈
V |
61 | 60 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ( lastS ‘𝑊) ∈ V) |
62 | | fvex 6113 |
. . . . . . . 8
⊢ (𝑈‘((#‘𝑈) − 2)) ∈
V |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈‘((#‘𝑈) − 2)) ∈ V) |
64 | | fvex 6113 |
. . . . . . . 8
⊢ ( lastS
‘𝑈) ∈
V |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ( lastS ‘𝑈) ∈ V) |
66 | | s2eq2s1eq 13531 |
. . . . . . 7
⊢ ((((𝑊‘((#‘𝑊) − 2)) ∈ V ∧ (
lastS ‘𝑊) ∈ V)
∧ ((𝑈‘((#‘𝑈) − 2)) ∈ V ∧ ( lastS
‘𝑈) ∈ V)) →
(〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉 =
〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉 ↔
(〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ∧
〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉))) |
67 | 59, 61, 63, 65, 66 | syl22anc 1319 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“(𝑊‘((#‘𝑊) − 2))( lastS ‘𝑊)”〉 =
〈“(𝑈‘((#‘𝑈) − 2))( lastS ‘𝑈)”〉 ↔
(〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ∧
〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉))) |
68 | | s111 13248 |
. . . . . . . . 9
⊢ (((𝑊‘((#‘𝑊) − 2)) ∈ V ∧
(𝑈‘((#‘𝑈) − 2)) ∈ V) →
(〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ↔ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑈) − 2)))) |
69 | 58, 63, 68 | sylancr 694 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ↔ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑈) − 2)))) |
70 | | oveq1 6556 |
. . . . . . . . . . . 12
⊢
((#‘𝑈) =
(#‘𝑊) →
((#‘𝑈) − 2) =
((#‘𝑊) −
2)) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . 11
⊢
((#‘𝑈) =
(#‘𝑊) → (𝑈‘((#‘𝑈) − 2)) = (𝑈‘((#‘𝑊) − 2))) |
72 | 71 | eqcoms 2618 |
. . . . . . . . . 10
⊢
((#‘𝑊) =
(#‘𝑈) → (𝑈‘((#‘𝑈) − 2)) = (𝑈‘((#‘𝑊) − 2))) |
73 | 72 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (𝑈‘((#‘𝑈) − 2)) = (𝑈‘((#‘𝑊) − 2))) |
74 | 73 | eqeq2d 2620 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑈) − 2)) ↔ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)))) |
75 | 69, 74 | bitrd 267 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ↔ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)))) |
76 | | s111 13248 |
. . . . . . . 8
⊢ ((( lastS
‘𝑊) ∈ V ∧ (
lastS ‘𝑈) ∈ V)
→ (〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉
↔ ( lastS ‘𝑊) =
( lastS ‘𝑈))) |
77 | 60, 65, 76 | sylancr 694 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (〈“( lastS ‘𝑊)”〉 = 〈“(
lastS ‘𝑈)”〉 ↔ ( lastS ‘𝑊) = ( lastS ‘𝑈))) |
78 | 75, 77 | anbi12d 743 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((〈“(𝑊‘((#‘𝑊) − 2))”〉 =
〈“(𝑈‘((#‘𝑈) − 2))”〉 ∧
〈“( lastS ‘𝑊)”〉 = 〈“( lastS
‘𝑈)”〉)
↔ ((𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))) |
79 | 57, 67, 78 | 3bitrd 293 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → ((𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) ↔ ((𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))) |
80 | 79 | anbi2d 736 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉)) ↔ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ ((𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS
‘𝑊) = ( lastS
‘𝑈))))) |
81 | | 3anass 1035 |
. . . 4
⊢ (((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS
‘𝑊) = ( lastS
‘𝑈)) ↔ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧
((𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS
‘𝑊) = ( lastS
‘𝑈)))) |
82 | 80, 81 | syl6bbr 277 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) ∧ (#‘𝑊) = (#‘𝑈)) → (((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉)) ↔ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈)))) |
83 | 82 | pm5.32da 671 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉) = (𝑈 substr 〈((#‘𝑊) − 2), (#‘𝑊)〉))) ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |
84 | 40, 83 | bitrd 267 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (#‘𝑊)) → (𝑊 = 𝑈 ↔ ((#‘𝑊) = (#‘𝑈) ∧ ((𝑊 substr 〈0, ((#‘𝑊) − 2)〉) = (𝑈 substr 〈0, ((#‘𝑊) − 2)〉) ∧ (𝑊‘((#‘𝑊) − 2)) = (𝑈‘((#‘𝑊) − 2)) ∧ ( lastS ‘𝑊) = ( lastS ‘𝑈))))) |