Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β πΈ:dom πΈβ1-1βπ
) |
2 | | simp1 1137 |
. . . . . . . 8
β’ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β π β Word dom πΈ) |
3 | 2 | adantr 482 |
. . . . . . 7
β’ (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β π β Word dom πΈ) |
4 | 1, 3 | anim12i 614 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (πΈ:dom πΈβ1-1βπ
β§ π β Word dom πΈ)) |
5 | | simp3 1139 |
. . . . . . 7
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β 2 β€
(β―βπ)) |
6 | | simpl2 1193 |
. . . . . . 7
β’ (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β π:(0...(β―βπ))βΆπ) |
7 | 5, 6 | anim12ci 615 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (π:(0...(β―βπ))βΆπ β§ 2 β€ (β―βπ))) |
8 | | simp3 1139 |
. . . . . . . 8
β’ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) |
9 | 8 | anim1i 616 |
. . . . . . 7
β’ (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β (βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπ)))) |
10 | 9 | adantl 483 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπ)))) |
11 | | clwlkclwwlklem2 29253 |
. . . . . 6
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word dom πΈ) β§ (π:(0...(β―βπ))βΆπ β§ 2 β€ (β―βπ)) β§ (βπ β
(0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπ)))) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)) |
12 | 4, 7, 10, 11 | syl3anc 1372 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)) |
13 | | lencl 14483 |
. . . . . . . 8
β’ (π β Word π β (β―βπ) β
β0) |
14 | | lencl 14483 |
. . . . . . . . . . . 12
β’ (π β Word dom πΈ β (β―βπ) β
β0) |
15 | | ffz0hash 14406 |
. . . . . . . . . . . . . . 15
β’
(((β―βπ)
β β0 β§ π:(0...(β―βπ))βΆπ) β (β―βπ) = ((β―βπ) + 1)) |
16 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ) =
((β―βπ) + 1)
β ((β―βπ)
β 1) = (((β―βπ) + 1) β 1)) |
17 | 16 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
((β―βπ) + 1)
β (((β―βπ)
β 1) β 0) = ((((β―βπ) + 1) β 1) β
0)) |
18 | | nn0cn 12482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ)
β β0 β (β―βπ) β β) |
19 | | peano2cn 11386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ)
β β β ((β―βπ) + 1) β β) |
20 | | peano2cnm 11526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((β―βπ)
+ 1) β β β (((β―βπ) + 1) β 1) β
β) |
21 | 18, 19, 20 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ)
β β0 β (((β―βπ) + 1) β 1) β
β) |
22 | 21 | subid1d 11560 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β0 β ((((β―βπ) + 1) β 1) β 0) =
(((β―βπ) + 1)
β 1)) |
23 | | 1cnd 11209 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ)
β β0 β 1 β β) |
24 | 18, 23 | pncand 11572 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β0 β (((β―βπ) + 1) β 1) = (β―βπ)) |
25 | 22, 24 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ)
β β0 β ((((β―βπ) + 1) β 1) β 0) =
(β―βπ)) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β―βπ)
β β0 β§ (β―βπ) β β0) β
((((β―βπ) + 1)
β 1) β 0) = (β―βπ)) |
27 | 17, 26 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (((β―βπ)
β 1) β 0) = (β―βπ)) |
28 | 27 | oveq1d 7424 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β ((((β―βπ)
β 1) β 0) β 1) = ((β―βπ) β 1)) |
29 | 28 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (0..^((((β―βπ) β 1) β 0) β 1)) =
(0..^((β―βπ)
β 1))) |
30 | 29 | raleqdv 3326 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
31 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ) =
((β―βπ) + 1)
β ((β―βπ)
β 2) = (((β―βπ) + 1) β 2)) |
32 | | 2cnd 12290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ)
β β0 β 2 β β) |
33 | 18, 32, 23 | subsub3d 11601 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β0 β ((β―βπ) β (2 β 1)) =
(((β―βπ) + 1)
β 2)) |
34 | | 2m1e1 12338 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (2
β 1) = 1 |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ)
β β0 β (2 β 1) = 1) |
36 | 35 | oveq2d 7425 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ)
β β0 β ((β―βπ) β (2 β 1)) =
((β―βπ) β
1)) |
37 | 33, 36 | eqtr3d 2775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ)
β β0 β (((β―βπ) + 1) β 2) = ((β―βπ) β 1)) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β―βπ)
β β0 β§ (β―βπ) β β0) β
(((β―βπ) + 1)
β 2) = ((β―βπ) β 1)) |
39 | 31, 38 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β ((β―βπ)
β 2) = ((β―βπ) β 1)) |
40 | 39 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (πβ((β―βπ) β 2)) = (πβ((β―βπ) β 1))) |
41 | 40 | preq1d 4744 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β {(πβ((β―βπ) β 2)), (πβ0)} = {(πβ((β―βπ) β 1)), (πβ0)}) |
42 | 41 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β ({(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ β {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)) |
43 | 30, 42 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β ((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))) |
44 | 43 | anbi2d 630 |
. . . . . . . . . . . . . . . . . 18
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
45 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . 18
β’
(((lastSβπ) =
(πβ0) β§
βπ β
(0..^((β―βπ)
β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))) |
46 | 44, 45 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
β’
((((β―βπ)
β β0 β§ (β―βπ) β β0) β§
(β―βπ) =
((β―βπ) + 1))
β (((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))) |
47 | 46 | expcom 415 |
. . . . . . . . . . . . . . . 16
β’
((β―βπ) =
((β―βπ) + 1)
β (((β―βπ)
β β0 β§ (β―βπ) β β0) β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
48 | 47 | expd 417 |
. . . . . . . . . . . . . . 15
β’
((β―βπ) =
((β―βπ) + 1)
β ((β―βπ)
β β0 β ((β―βπ) β β0 β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))))) |
49 | 15, 48 | syl 17 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
β β0 β§ π:(0...(β―βπ))βΆπ) β ((β―βπ) β β0 β
((β―βπ) β
β0 β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))))) |
50 | 49 | ex 414 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β (π:(0...(β―βπ))βΆπ β ((β―βπ) β β0 β
((β―βπ) β
β0 β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))))) |
51 | 50 | com23 86 |
. . . . . . . . . . . 12
β’
((β―βπ)
β β0 β ((β―βπ) β β0 β (π:(0...(β―βπ))βΆπ β ((β―βπ) β β0 β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))))) |
52 | 14, 14, 51 | sylc 65 |
. . . . . . . . . . 11
β’ (π β Word dom πΈ β (π:(0...(β―βπ))βΆπ β ((β―βπ) β β0 β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))))) |
53 | 52 | imp 408 |
. . . . . . . . . 10
β’ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ) β ((β―βπ) β β0 β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
54 | 53 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β ((β―βπ) β β0
β (((lastSβπ) =
(πβ0) β§
(βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
55 | 54 | adantr 482 |
. . . . . . . 8
β’ (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((β―βπ) β β0 β
(((lastSβπ) = (πβ0) β§ (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
56 | 13, 55 | syl5com 31 |
. . . . . . 7
β’ (π β Word π β (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
57 | 56 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ)))) |
58 | 57 | imp 408 |
. . . . 5
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ βπ β (0..^((β―βπ) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 1)), (πβ0)} β ran πΈ))) |
59 | 12, 58 | mpbird 257 |
. . . 4
β’ (((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β§ ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ)))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) |
60 | 59 | ex 414 |
. . 3
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) |
61 | 60 | exlimdv 1937 |
. 2
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) |
62 | | clwlkclwwlklem1 29252 |
. 2
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
63 | 61, 62 | impbid 211 |
1
β’ ((πΈ:dom πΈβ1-1βπ
β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) |