Proof of Theorem 2swrd2eqwrdeq
| Step | Hyp | Ref
| Expression |
| 1 | | lencl 14571 |
. . . . 5
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∈
ℕ0) |
| 2 | | 1z 12647 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
| 3 | | nn0z 12638 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ ℤ) |
| 4 | | zltp1le 12667 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ (♯‘𝑊) ∈ ℤ) → (1 <
(♯‘𝑊) ↔ (1
+ 1) ≤ (♯‘𝑊))) |
| 5 | 2, 3, 4 | sylancr 587 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ0 → (1 < (♯‘𝑊) ↔ (1 + 1) ≤ (♯‘𝑊))) |
| 6 | | 1p1e2 12391 |
. . . . . . . . . . . 12
⊢ (1 + 1) =
2 |
| 7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((♯‘𝑊)
∈ ℕ0 → (1 + 1) = 2) |
| 8 | 7 | breq1d 5153 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 → ((1 + 1) ≤ (♯‘𝑊) ↔ 2 ≤
(♯‘𝑊))) |
| 9 | 8 | biimpd 229 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ0 → ((1 + 1) ≤ (♯‘𝑊) → 2 ≤
(♯‘𝑊))) |
| 10 | 5, 9 | sylbid 240 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 → (1 < (♯‘𝑊) → 2 ≤ (♯‘𝑊))) |
| 11 | 10 | imp 406 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → 2 ≤ (♯‘𝑊)) |
| 12 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 13 | | simpl 482 |
. . . . . . . 8
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → (♯‘𝑊) ∈
ℕ0) |
| 14 | | nn0sub 12576 |
. . . . . . . 8
⊢ ((2
∈ ℕ0 ∧ (♯‘𝑊) ∈ ℕ0) → (2 ≤
(♯‘𝑊) ↔
((♯‘𝑊) −
2) ∈ ℕ0)) |
| 15 | 12, 13, 14 | sylancr 587 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → (2 ≤ (♯‘𝑊) ↔ ((♯‘𝑊) − 2) ∈
ℕ0)) |
| 16 | 11, 15 | mpbid 232 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → ((♯‘𝑊) − 2) ∈
ℕ0) |
| 17 | 3 | adantr 480 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → (♯‘𝑊) ∈ ℤ) |
| 18 | | 0red 11264 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 → 0 ∈ ℝ) |
| 19 | | 1red 11262 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 → 1 ∈ ℝ) |
| 20 | | nn0re 12535 |
. . . . . . . . . 10
⊢
((♯‘𝑊)
∈ ℕ0 → (♯‘𝑊) ∈ ℝ) |
| 21 | 18, 19, 20 | 3jca 1129 |
. . . . . . . . 9
⊢
((♯‘𝑊)
∈ ℕ0 → (0 ∈ ℝ ∧ 1 ∈ ℝ
∧ (♯‘𝑊)
∈ ℝ)) |
| 22 | | 0lt1 11785 |
. . . . . . . . 9
⊢ 0 <
1 |
| 23 | | lttr 11337 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → ((0 < 1 ∧ 1
< (♯‘𝑊))
→ 0 < (♯‘𝑊))) |
| 24 | 23 | expd 415 |
. . . . . . . . 9
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ (♯‘𝑊) ∈ ℝ) → (0 < 1 → (1
< (♯‘𝑊)
→ 0 < (♯‘𝑊)))) |
| 25 | 21, 22, 24 | mpisyl 21 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 → (1 < (♯‘𝑊) → 0 < (♯‘𝑊))) |
| 26 | 25 | imp 406 |
. . . . . . 7
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → 0 < (♯‘𝑊)) |
| 27 | | elnnz 12623 |
. . . . . . 7
⊢
((♯‘𝑊)
∈ ℕ ↔ ((♯‘𝑊) ∈ ℤ ∧ 0 <
(♯‘𝑊))) |
| 28 | 17, 26, 27 | sylanbrc 583 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → (♯‘𝑊) ∈ ℕ) |
| 29 | | 2rp 13039 |
. . . . . . . . 9
⊢ 2 ∈
ℝ+ |
| 30 | 29 | a1i 11 |
. . . . . . . 8
⊢
((♯‘𝑊)
∈ ℕ0 → 2 ∈
ℝ+) |
| 31 | 20, 30 | ltsubrpd 13109 |
. . . . . . 7
⊢
((♯‘𝑊)
∈ ℕ0 → ((♯‘𝑊) − 2) < (♯‘𝑊)) |
| 32 | 31 | adantr 480 |
. . . . . 6
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → ((♯‘𝑊) − 2) < (♯‘𝑊)) |
| 33 | | elfzo0 13740 |
. . . . . 6
⊢
(((♯‘𝑊)
− 2) ∈ (0..^(♯‘𝑊)) ↔ (((♯‘𝑊) − 2) ∈ ℕ0
∧ (♯‘𝑊)
∈ ℕ ∧ ((♯‘𝑊) − 2) < (♯‘𝑊))) |
| 34 | 16, 28, 32, 33 | syl3anbrc 1344 |
. . . . 5
⊢
(((♯‘𝑊)
∈ ℕ0 ∧ 1 < (♯‘𝑊)) → ((♯‘𝑊) − 2) ∈
(0..^(♯‘𝑊))) |
| 35 | 1, 34 | sylan 580 |
. . . 4
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → ((♯‘𝑊) − 2) ∈
(0..^(♯‘𝑊))) |
| 36 | 35 | 3adant2 1132 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → ((♯‘𝑊) − 2) ∈
(0..^(♯‘𝑊))) |
| 37 | | pfxsuffeqwrdeq 14736 |
. . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ ((♯‘𝑊) − 2) ∈
(0..^(♯‘𝑊)))
→ (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉))))) |
| 38 | 36, 37 | syld3an3 1411 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉))))) |
| 39 | | swrd2lsw 14991 |
. . . . . . . . 9
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉) |
| 40 | 39 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉) |
| 41 | 40 | adantr 480 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉) |
| 42 | | breq2 5147 |
. . . . . . . . . . 11
⊢
((♯‘𝑊) =
(♯‘𝑈) → (1
< (♯‘𝑊)
↔ 1 < (♯‘𝑈))) |
| 43 | 42 | 3anbi3d 1444 |
. . . . . . . . . 10
⊢
((♯‘𝑊) =
(♯‘𝑈) →
((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ↔ (𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑈)))) |
| 44 | | swrd2lsw 14991 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑈)) → (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉) |
| 45 | 44 | 3adant1 1131 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑈)) → (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉) |
| 46 | 43, 45 | biimtrdi 253 |
. . . . . . . . 9
⊢
((♯‘𝑊) =
(♯‘𝑈) →
((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉)) |
| 47 | 46 | impcom 407 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉) |
| 48 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊) =
(♯‘𝑈) →
((♯‘𝑊) −
2) = ((♯‘𝑈)
− 2)) |
| 49 | | id 22 |
. . . . . . . . . . . 12
⊢
((♯‘𝑊) =
(♯‘𝑈) →
(♯‘𝑊) =
(♯‘𝑈)) |
| 50 | 48, 49 | opeq12d 4881 |
. . . . . . . . . . 11
⊢
((♯‘𝑊) =
(♯‘𝑈) →
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉 = 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) |
| 51 | 50 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((♯‘𝑊) =
(♯‘𝑈) →
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉) = (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉)) |
| 52 | 51 | eqeq1d 2739 |
. . . . . . . . 9
⊢
((♯‘𝑊) =
(♯‘𝑈) →
((𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉) = 〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉 ↔ (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉)) |
| 53 | 52 | adantl 481 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → ((𝑈 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉 ↔ (𝑈 substr 〈((♯‘𝑈) − 2),
(♯‘𝑈)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉)) |
| 54 | 47, 53 | mpbird 257 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑈 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉) |
| 55 | 41, 54 | eqeq12d 2753 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → ((𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉) ↔ 〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉)) |
| 56 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑊‘((♯‘𝑊) − 2)) ∈ V) |
| 57 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (lastS‘𝑊) ∈ V) |
| 58 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑈‘((♯‘𝑈) − 2)) ∈ V) |
| 59 | | fvexd 6921 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (lastS‘𝑈) ∈ V) |
| 60 | | s2eq2s1eq 14975 |
. . . . . . 7
⊢ ((((𝑊‘((♯‘𝑊) − 2)) ∈ V ∧
(lastS‘𝑊) ∈ V)
∧ ((𝑈‘((♯‘𝑈) − 2)) ∈ V ∧
(lastS‘𝑈) ∈ V))
→ (〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉 = 〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉 ↔
(〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ∧
〈“(lastS‘𝑊)”〉 =
〈“(lastS‘𝑈)”〉))) |
| 61 | 56, 57, 58, 59, 60 | syl22anc 839 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (〈“(𝑊‘((♯‘𝑊) − 2))(lastS‘𝑊)”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))(lastS‘𝑈)”〉 ↔ (〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ∧
〈“(lastS‘𝑊)”〉 =
〈“(lastS‘𝑈)”〉))) |
| 62 | | fvex 6919 |
. . . . . . . . 9
⊢ (𝑊‘((♯‘𝑊) − 2)) ∈
V |
| 63 | | s111 14653 |
. . . . . . . . 9
⊢ (((𝑊‘((♯‘𝑊) − 2)) ∈ V ∧
(𝑈‘((♯‘𝑈) − 2)) ∈ V) →
(〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ↔ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑈) − 2)))) |
| 64 | 62, 58, 63 | sylancr 587 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ↔ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑈) − 2)))) |
| 65 | | fvoveq1 7454 |
. . . . . . . . . . 11
⊢
((♯‘𝑈) =
(♯‘𝑊) →
(𝑈‘((♯‘𝑈) − 2)) = (𝑈‘((♯‘𝑊) − 2))) |
| 66 | 65 | eqcoms 2745 |
. . . . . . . . . 10
⊢
((♯‘𝑊) =
(♯‘𝑈) →
(𝑈‘((♯‘𝑈) − 2)) = (𝑈‘((♯‘𝑊) − 2))) |
| 67 | 66 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (𝑈‘((♯‘𝑈) − 2)) = (𝑈‘((♯‘𝑊) − 2))) |
| 68 | 67 | eqeq2d 2748 |
. . . . . . . 8
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → ((𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑈) − 2)) ↔ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)))) |
| 69 | 64, 68 | bitrd 279 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ↔ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)))) |
| 70 | | fvex 6919 |
. . . . . . . 8
⊢
(lastS‘𝑊)
∈ V |
| 71 | | s111 14653 |
. . . . . . . 8
⊢
(((lastS‘𝑊)
∈ V ∧ (lastS‘𝑈) ∈ V) →
(〈“(lastS‘𝑊)”〉 =
〈“(lastS‘𝑈)”〉 ↔ (lastS‘𝑊) = (lastS‘𝑈))) |
| 72 | 70, 59, 71 | sylancr 587 |
. . . . . . 7
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) →
(〈“(lastS‘𝑊)”〉 =
〈“(lastS‘𝑈)”〉 ↔ (lastS‘𝑊) = (lastS‘𝑈))) |
| 73 | 69, 72 | anbi12d 632 |
. . . . . 6
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → ((〈“(𝑊‘((♯‘𝑊) − 2))”〉 =
〈“(𝑈‘((♯‘𝑈) − 2))”〉 ∧
〈“(lastS‘𝑊)”〉 =
〈“(lastS‘𝑈)”〉) ↔ ((𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))) |
| 74 | 55, 61, 73 | 3bitrd 305 |
. . . . 5
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → ((𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉) ↔ ((𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))) |
| 75 | 74 | anbi2d 630 |
. . . 4
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉)) ↔ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ ((𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈))))) |
| 76 | | 3anass 1095 |
. . . 4
⊢ (((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧
(lastS‘𝑊) =
(lastS‘𝑈)) ↔
((𝑊 prefix
((♯‘𝑊) −
2)) = (𝑈 prefix
((♯‘𝑊) −
2)) ∧ ((𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))) |
| 77 | 75, 76 | bitr4di 289 |
. . 3
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) ∧ (♯‘𝑊) = (♯‘𝑈)) → (((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉)) ↔ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈)))) |
| 78 | 77 | pm5.32da 579 |
. 2
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊 substr 〈((♯‘𝑊) − 2),
(♯‘𝑊)〉) =
(𝑈 substr
〈((♯‘𝑊)
− 2), (♯‘𝑊)〉))) ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈))))) |
| 79 | 38, 78 | bitrd 279 |
1
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉 ∧ 1 < (♯‘𝑊)) → (𝑊 = 𝑈 ↔ ((♯‘𝑊) = (♯‘𝑈) ∧ ((𝑊 prefix ((♯‘𝑊) − 2)) = (𝑈 prefix ((♯‘𝑊) − 2)) ∧ (𝑊‘((♯‘𝑊) − 2)) = (𝑈‘((♯‘𝑊) − 2)) ∧ (lastS‘𝑊) = (lastS‘𝑈))))) |