Step | Hyp | Ref
| Expression |
1 | | ccats1pfxeq 14609 |
. 2
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) |
2 | | simp1 1137 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π β Word π) |
3 | | lencl 14428 |
. . . . . . . . 9
β’ (π β Word π β (β―βπ) β
β0) |
4 | | nn0p1nn 12459 |
. . . . . . . . 9
β’
((β―βπ)
β β0 β ((β―βπ) + 1) β β) |
5 | 3, 4 | syl 17 |
. . . . . . . 8
β’ (π β Word π β ((β―βπ) + 1) β β) |
6 | 5 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β ((β―βπ) + 1) β
β) |
7 | | 3simpc 1151 |
. . . . . . 7
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π β Word π β§ (β―βπ) = ((β―βπ) + 1))) |
8 | | lswlgt0cl 14464 |
. . . . . . 7
β’
((((β―βπ)
+ 1) β β β§ (π β Word π β§ (β―βπ) = ((β―βπ) + 1))) β (lastSβπ) β π) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . 6
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (lastSβπ) β π) |
10 | 9 | s1cld 14498 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β
β¨β(lastSβπ)ββ© β Word π) |
11 | | eqidd 2738 |
. . . . 5
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (β―βπ) = (β―βπ)) |
12 | | pfxccatid 14636 |
. . . . . 6
β’ ((π β Word π β§ β¨β(lastSβπ)ββ© β Word π β§ (β―βπ) = (β―βπ)) β ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ)) = π) |
13 | 12 | eqcomd 2743 |
. . . . 5
β’ ((π β Word π β§ β¨β(lastSβπ)ββ© β Word π β§ (β―βπ) = (β―βπ)) β π = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
14 | 2, 10, 11, 13 | syl3anc 1372 |
. . . 4
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β π = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
15 | | oveq1 7369 |
. . . . 5
β’ (π = (π ++ β¨β(lastSβπ)ββ©) β (π prefix (β―βπ)) = ((π ++ β¨β(lastSβπ)ββ©) prefix
(β―βπ))) |
16 | 15 | eqcomd 2743 |
. . . 4
β’ (π = (π ++ β¨β(lastSβπ)ββ©) β ((π ++
β¨β(lastSβπ)ββ©) prefix (β―βπ)) = (π prefix (β―βπ))) |
17 | 14, 16 | sylan9eq 2797 |
. . 3
β’ (((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β§ π = (π ++ β¨β(lastSβπ)ββ©)) β π = (π prefix (β―βπ))) |
18 | 17 | ex 414 |
. 2
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π ++ β¨β(lastSβπ)ββ©) β π = (π prefix (β―βπ)))) |
19 | 1, 18 | impbid 211 |
1
β’ ((π β Word π β§ π β Word π β§ (β―βπ) = ((β―βπ) + 1)) β (π = (π prefix (β―βπ)) β π = (π ++ β¨β(lastSβπ)ββ©))) |