Step | Hyp | Ref
| Expression |
1 | | iwrdsplit.s |
. . . 4
β’ (π β π β V) |
2 | | iwrdsplit.f |
. . . 4
β’ (π β πΉ:β0βΆπ) |
3 | | iwrdsplit.n |
. . . . 5
β’ (π β π β
β0) |
4 | | 1nn0 12436 |
. . . . . 6
β’ 1 β
β0 |
5 | 4 | a1i 11 |
. . . . 5
β’ (π β 1 β
β0) |
6 | 3, 5 | nn0addcld 12484 |
. . . 4
β’ (π β (π + 1) β
β0) |
7 | 1, 2, 6 | subiwrd 33025 |
. . 3
β’ (π β (πΉ βΎ (0..^(π + 1))) β Word π) |
8 | | 1re 11162 |
. . . . . 6
β’ 1 β
β |
9 | | nn0addge2 12467 |
. . . . . 6
β’ ((1
β β β§ π
β β0) β 1 β€ (π + 1)) |
10 | 8, 3, 9 | sylancr 588 |
. . . . 5
β’ (π β 1 β€ (π + 1)) |
11 | 1, 2, 6 | subiwrdlen 33026 |
. . . . 5
β’ (π β (β―β(πΉ βΎ (0..^(π + 1)))) = (π + 1)) |
12 | 10, 11 | breqtrrd 5138 |
. . . 4
β’ (π β 1 β€
(β―β(πΉ βΎ
(0..^(π +
1))))) |
13 | | wrdlenge1n0 14445 |
. . . . 5
β’ ((πΉ βΎ (0..^(π + 1))) β Word π β ((πΉ βΎ (0..^(π + 1))) β β
β 1 β€
(β―β(πΉ βΎ
(0..^(π +
1)))))) |
14 | 7, 13 | syl 17 |
. . . 4
β’ (π β ((πΉ βΎ (0..^(π + 1))) β β
β 1 β€
(β―β(πΉ βΎ
(0..^(π +
1)))))) |
15 | 12, 14 | mpbird 257 |
. . 3
β’ (π β (πΉ βΎ (0..^(π + 1))) β β
) |
16 | | pfxlswccat 14608 |
. . 3
β’ (((πΉ βΎ (0..^(π + 1))) β Word π β§ (πΉ βΎ (0..^(π + 1))) β β
) β (((πΉ βΎ (0..^(π + 1))) prefix ((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) ++
β¨β(lastSβ(πΉ βΎ (0..^(π + 1))))ββ©) = (πΉ βΎ (0..^(π + 1)))) |
17 | 7, 15, 16 | syl2anc 585 |
. 2
β’ (π β (((πΉ βΎ (0..^(π + 1))) prefix ((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) ++
β¨β(lastSβ(πΉ βΎ (0..^(π + 1))))ββ©) = (πΉ βΎ (0..^(π + 1)))) |
18 | 3 | nn0cnd 12482 |
. . . . . 6
β’ (π β π β β) |
19 | | 1cnd 11157 |
. . . . . 6
β’ (π β 1 β
β) |
20 | 18, 19, 11 | mvrraddd 11574 |
. . . . 5
β’ (π β ((β―β(πΉ βΎ (0..^(π + 1)))) β 1) = π) |
21 | 20 | oveq2d 7378 |
. . . 4
β’ (π β ((πΉ βΎ (0..^(π + 1))) prefix ((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) = ((πΉ βΎ (0..^(π + 1))) prefix π)) |
22 | | nn0fz0 13546 |
. . . . . . . 8
β’ (π β β0
β π β (0...π)) |
23 | 3, 22 | sylib 217 |
. . . . . . 7
β’ (π β π β (0...π)) |
24 | | elfz0add 13547 |
. . . . . . . 8
β’ ((π β β0
β§ 1 β β0) β (π β (0...π) β π β (0...(π + 1)))) |
25 | 24 | imp 408 |
. . . . . . 7
β’ (((π β β0
β§ 1 β β0) β§ π β (0...π)) β π β (0...(π + 1))) |
26 | 3, 5, 23, 25 | syl21anc 837 |
. . . . . 6
β’ (π β π β (0...(π + 1))) |
27 | 11 | oveq2d 7378 |
. . . . . 6
β’ (π β (0...(β―β(πΉ βΎ (0..^(π + 1))))) = (0...(π + 1))) |
28 | 26, 27 | eleqtrrd 2841 |
. . . . 5
β’ (π β π β (0...(β―β(πΉ βΎ (0..^(π + 1)))))) |
29 | | pfxres 14574 |
. . . . 5
β’ (((πΉ βΎ (0..^(π + 1))) β Word π β§ π β (0...(β―β(πΉ βΎ (0..^(π + 1)))))) β ((πΉ βΎ (0..^(π + 1))) prefix π) = ((πΉ βΎ (0..^(π + 1))) βΎ (0..^π))) |
30 | 7, 28, 29 | syl2anc 585 |
. . . 4
β’ (π β ((πΉ βΎ (0..^(π + 1))) prefix π) = ((πΉ βΎ (0..^(π + 1))) βΎ (0..^π))) |
31 | | fzossfzop1 13657 |
. . . . 5
β’ (π β β0
β (0..^π) β
(0..^(π +
1))) |
32 | | resabs1 5972 |
. . . . 5
β’
((0..^π) β
(0..^(π + 1)) β
((πΉ βΎ (0..^(π + 1))) βΎ (0..^π)) = (πΉ βΎ (0..^π))) |
33 | 3, 31, 32 | 3syl 18 |
. . . 4
β’ (π β ((πΉ βΎ (0..^(π + 1))) βΎ (0..^π)) = (πΉ βΎ (0..^π))) |
34 | 21, 30, 33 | 3eqtrd 2781 |
. . 3
β’ (π β ((πΉ βΎ (0..^(π + 1))) prefix ((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) = (πΉ βΎ (0..^π))) |
35 | | lsw 14459 |
. . . . . 6
β’ ((πΉ βΎ (0..^(π + 1))) β Word π β (lastSβ(πΉ βΎ (0..^(π + 1)))) = ((πΉ βΎ (0..^(π + 1)))β((β―β(πΉ βΎ (0..^(π + 1)))) β 1))) |
36 | 7, 35 | syl 17 |
. . . . 5
β’ (π β (lastSβ(πΉ βΎ (0..^(π + 1)))) = ((πΉ βΎ (0..^(π + 1)))β((β―β(πΉ βΎ (0..^(π + 1)))) β 1))) |
37 | 20 | fveq2d 6851 |
. . . . 5
β’ (π β ((πΉ βΎ (0..^(π + 1)))β((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) = ((πΉ βΎ (0..^(π + 1)))βπ)) |
38 | | fzonn0p1 13656 |
. . . . . 6
β’ (π β β0
β π β (0..^(π + 1))) |
39 | | fvres 6866 |
. . . . . 6
β’ (π β (0..^(π + 1)) β ((πΉ βΎ (0..^(π + 1)))βπ) = (πΉβπ)) |
40 | 3, 38, 39 | 3syl 18 |
. . . . 5
β’ (π β ((πΉ βΎ (0..^(π + 1)))βπ) = (πΉβπ)) |
41 | 36, 37, 40 | 3eqtrd 2781 |
. . . 4
β’ (π β (lastSβ(πΉ βΎ (0..^(π + 1)))) = (πΉβπ)) |
42 | 41 | s1eqd 14496 |
. . 3
β’ (π β
β¨β(lastSβ(πΉ βΎ (0..^(π + 1))))ββ© = β¨β(πΉβπ)ββ©) |
43 | 34, 42 | oveq12d 7380 |
. 2
β’ (π β (((πΉ βΎ (0..^(π + 1))) prefix ((β―β(πΉ βΎ (0..^(π + 1)))) β 1)) ++
β¨β(lastSβ(πΉ βΎ (0..^(π + 1))))ββ©) = ((πΉ βΎ (0..^π)) ++ β¨β(πΉβπ)ββ©)) |
44 | 17, 43 | eqtr3d 2779 |
1
β’ (π β (πΉ βΎ (0..^(π + 1))) = ((πΉ βΎ (0..^π)) ++ β¨β(πΉβπ)ββ©)) |