Step | Hyp | Ref
| Expression |
1 | | hashgt0n0 14272 |
. . . . . 6
β’ ((π β Word π β§ 0 < (β―βπ)) β π β β
) |
2 | | lennncl 14429 |
. . . . . 6
β’ ((π β Word π β§ π β β
) β (β―βπ) β
β) |
3 | 1, 2 | syldan 592 |
. . . . 5
β’ ((π β Word π β§ 0 < (β―βπ)) β (β―βπ) β
β) |
4 | 3 | 3adant2 1132 |
. . . 4
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (β―βπ) β
β) |
5 | | fzo0end 13671 |
. . . 4
β’
((β―βπ)
β β β ((β―βπ) β 1) β
(0..^(β―βπ))) |
6 | 4, 5 | syl 17 |
. . 3
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β ((β―βπ) β 1) β
(0..^(β―βπ))) |
7 | | pfxsuffeqwrdeq 14593 |
. . 3
β’ ((π β Word π β§ π β Word π β§ ((β―βπ) β 1) β
(0..^(β―βπ)))
β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©))))) |
8 | 6, 7 | syld3an3 1410 |
. 2
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©))))) |
9 | | hashneq0 14271 |
. . . . . . . . . . 11
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
10 | 9 | biimpd 228 |
. . . . . . . . . 10
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
11 | 10 | imdistani 570 |
. . . . . . . . 9
β’ ((π β Word π β§ 0 < (β―βπ)) β (π β Word π β§ π β β
)) |
12 | 11 | 3adant2 1132 |
. . . . . . . 8
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π β Word π β§ π β β
)) |
13 | 12 | adantr 482 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π β Word π β§ π β β
)) |
14 | | swrdlsw 14562 |
. . . . . . 7
β’ ((π β Word π β§ π β β
) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
16 | | breq2 5114 |
. . . . . . . . . 10
β’
((β―βπ) =
(β―βπ) β (0
< (β―βπ)
β 0 < (β―βπ))) |
17 | 16 | 3anbi3d 1443 |
. . . . . . . . 9
β’
((β―βπ) =
(β―βπ) β
((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π β Word π β§ π β Word π β§ 0 < (β―βπ)))) |
18 | | hashneq0 14271 |
. . . . . . . . . . . . 13
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
19 | 18 | biimpd 228 |
. . . . . . . . . . . 12
β’ (π β Word π β (0 < (β―βπ) β π β β
)) |
20 | 19 | imdistani 570 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 0 < (β―βπ)) β (π β Word π β§ π β β
)) |
21 | 20 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π β Word π β§ π β β
)) |
22 | | swrdlsw 14562 |
. . . . . . . . . 10
β’ ((π β Word π β§ π β β
) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
24 | 17, 23 | syl6bi 253 |
. . . . . . . 8
β’
((β―βπ) =
(β―βπ) β
((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©)) |
25 | 24 | impcom 409 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
26 | | oveq1 7369 |
. . . . . . . . . . 11
β’
((β―βπ) =
(β―βπ) β
((β―βπ) β
1) = ((β―βπ)
β 1)) |
27 | | id 22 |
. . . . . . . . . . 11
β’
((β―βπ) =
(β―βπ) β
(β―βπ) =
(β―βπ)) |
28 | 26, 27 | opeq12d 4843 |
. . . . . . . . . 10
β’
((β―βπ) =
(β―βπ) β
β¨((β―βπ)
β 1), (β―βπ)β© = β¨((β―βπ) β 1),
(β―βπ)β©) |
29 | 28 | oveq2d 7378 |
. . . . . . . . 9
β’
((β―βπ) =
(β―βπ) β
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©) = (π substr β¨((β―βπ) β 1),
(β―βπ)β©)) |
30 | 29 | eqeq1d 2739 |
. . . . . . . 8
β’
((β―βπ) =
(β―βπ) β
((π substr
β¨((β―βπ)
β 1), (β―βπ)β©) = β¨β(lastSβπ)ββ© β (π substr
β¨((β―βπ)
β 1), (β―βπ)β©) = β¨β(lastSβπ)ββ©)) |
31 | 30 | adantl 483 |
. . . . . . 7
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ© β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©)) |
32 | 25, 31 | mpbird 257 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
β¨β(lastSβπ)ββ©) |
33 | 15, 32 | eqeq12d 2753 |
. . . . 5
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©) β
β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ©)) |
34 | | fvexd 6862 |
. . . . . 6
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (lastSβπ) β V) |
35 | | fvex 6860 |
. . . . . 6
β’
(lastSβπ)
β V |
36 | | s111 14510 |
. . . . . 6
β’
(((lastSβπ)
β V β§ (lastSβπ) β V) β
(β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ© β (lastSβπ) = (lastSβπ))) |
37 | 34, 35, 36 | sylancl 587 |
. . . . 5
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β
(β¨β(lastSβπ)ββ© =
β¨β(lastSβπ)ββ© β (lastSβπ) = (lastSβπ))) |
38 | 33, 37 | bitrd 279 |
. . . 4
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β ((π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©) β (lastSβπ) = (lastSβπ))) |
39 | 38 | anbi2d 630 |
. . 3
β’ (((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β§ (β―βπ) = (β―βπ)) β (((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©)) β ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (lastSβπ) = (lastSβπ)))) |
40 | 39 | pm5.32da 580 |
. 2
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (π substr β¨((β―βπ) β 1),
(β―βπ)β©) =
(π substr
β¨((β―βπ)
β 1), (β―βπ)β©))) β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (lastSβπ) = (lastSβπ))))) |
41 | 8, 40 | bitrd 279 |
1
β’ ((π β Word π β§ π β Word π β§ 0 < (β―βπ)) β (π = π β ((β―βπ) = (β―βπ) β§ ((π prefix ((β―βπ) β 1)) = (π prefix ((β―βπ) β 1)) β§ (lastSβπ) = (lastSβπ))))) |