Step | Hyp | Ref
| Expression |
1 | | ccats1pfxeq 14688 |
. 2
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) |
2 | | simp1 1134 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π β Word π) |
3 | | lencl 14507 |
. . . . . . . . 9
β’ (π β Word π β (β―βπ) β
β0) |
4 | | nn0p1nn 12533 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((β―βπ) + 1) β β) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β Word π β ((β―βπ) + 1) β β) |
6 | 5 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β ((β―βπ) + 1) β
β) |
7 | | 3simpc 1148 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π β Word π β§ (β―βπ) = ((β―βπ) + 1))) |
8 | | lswlgt0cl 14543 |
. . . . . . 7
β’
((((β―βπ)
+ 1) β β β§ (π β Word π β§ (β―βπ) = ((β―βπ) + 1))) β (lastSβπ) β π) |
9 | 6, 7, 8 | syl2anc 583 |
. . . . . 6
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (lastSβπ) β π) |
10 | 9 | s1cld 14577 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β
β¨β(lastSβπ)ββ© β Word π) |
11 | | eqidd 2728 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (β―βπ) = (β―βπ)) |
12 | | pfxccatid 14715 |
. . . . . 6
β’ ((π β Word π β§ β¨β(lastSβπ)ββ© β Word π β§ (β―βπ) = (β―βπ)) β ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ)) = π) |
13 | 12 | eqcomd 2733 |
. . . . 5
β’ ((π β Word π β§ β¨β(lastSβπ)ββ© β Word π β§ (β―βπ) = (β―βπ)) β π = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
14 | 2, 10, 11, 13 | syl3anc 1369 |
. . . 4
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
15 | | oveq1 7421 |
. . . . 5
β’ (π = (π ++ β¨β(lastSβπ)ββ©) β (π prefix (β―βπ)) = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
16 | 15 | eqcomd 2733 |
. . . 4
β’ (π = (π ++ β¨β(lastSβπ)ββ©) β ((π ++
β¨β(lastSβπ)ββ©) prefix (β―βπ)) = (π prefix (β―βπ))) |
17 | 14, 16 | sylan9eq 2787 |
. . 3
β’ (((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β§ π = (π ++ β¨β(lastSβπ)ββ©)) β π = (π prefix (β―βπ))) |
18 | 17 | ex 412 |
. 2
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π ++ β¨β(lastSβπ)ββ©) β π = (π prefix (β―βπ)))) |
19 | 1, 18 | impbid 211 |
1
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) |