Step | Hyp | Ref
| Expression |
1 | | clwlkclwwlk.e |
. . . . . 6
β’ πΈ = (iEdgβπΊ) |
2 | 1 | uspgrf1oedg 28173 |
. . . . 5
β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ)) |
3 | | f1of1 6787 |
. . . . 5
β’ (πΈ:dom πΈβ1-1-ontoβ(EdgβπΊ) β πΈ:dom πΈβ1-1β(EdgβπΊ)) |
4 | 2, 3 | syl 17 |
. . . 4
β’ (πΊ β USPGraph β πΈ:dom πΈβ1-1β(EdgβπΊ)) |
5 | | clwlkclwwlklem3 28994 |
. . . 4
β’ ((πΈ:dom πΈβ1-1β(EdgβπΊ) β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) |
6 | 4, 5 | syl3an1 1164 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)))) |
7 | | lencl 14430 |
. . . . . . . . . . . . . 14
β’ (π β Word π β (β―βπ) β
β0) |
8 | | ige2m1fz 13540 |
. . . . . . . . . . . . . 14
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
(0...(β―βπ))) |
9 | 7, 8 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
(0...(β―βπ))) |
10 | | pfxlen 14580 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ ((β―βπ) β 1) β
(0...(β―βπ)))
β (β―β(π
prefix ((β―βπ)
β 1))) = ((β―βπ) β 1)) |
11 | 9, 10 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―β(π prefix ((β―βπ) β 1))) =
((β―βπ) β
1)) |
12 | 7 | nn0cnd 12483 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β (β―βπ) β β) |
13 | | 1cnd 11158 |
. . . . . . . . . . . . . . . 16
β’ (π β Word π β 1 β β) |
14 | 12, 13 | subcld 11520 |
. . . . . . . . . . . . . . 15
β’ (π β Word π β ((β―βπ) β 1) β
β) |
15 | 14 | subid1d 11509 |
. . . . . . . . . . . . . 14
β’ (π β Word π β (((β―βπ) β 1) β 0) =
((β―βπ) β
1)) |
16 | 15 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (π β Word π β ((β―βπ) β 1) = (((β―βπ) β 1) β
0)) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) =
(((β―βπ) β
1) β 0)) |
18 | 11, 17 | eqtrd 2773 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―β(π prefix ((β―βπ) β 1))) =
(((β―βπ) β
1) β 0)) |
19 | 18 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―β(π prefix ((β―βπ) β 1))) β 1) =
((((β―βπ)
β 1) β 0) β 1)) |
20 | 19 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)) = (0..^((((β―βπ) β 1) β 0) β
1))) |
21 | 11 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―β(π prefix ((β―βπ) β 1))) β 1) =
(((β―βπ) β
1) β 1)) |
22 | 21 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ ((π β Word π β§ 2 β€ (β―βπ)) β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)) = (0..^(((β―βπ) β 1) β 1))) |
23 | 22 | eleq2d 2820 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π β (0..^((β―β(π prefix ((β―βπ) β 1))) β 1))
β π β
(0..^(((β―βπ)
β 1) β 1)))) |
24 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
π β Word π) |
25 | | wrdlenge2n0 14449 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π β β
) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
π β
β
) |
27 | | nn0z 12532 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ)
β β0 β (β―βπ) β β€) |
28 | | peano2zm 12554 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ)
β β€ β ((β―βπ) β 1) β
β€) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β
β€) |
30 | 7, 29 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β Word π β ((β―βπ) β 1) β
β€) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
β€) |
32 | | elfzom1elfzo 13649 |
. . . . . . . . . . . . . . . 16
β’
((((β―βπ)
β 1) β β€ β§ π β (0..^(((β―βπ) β 1) β 1))) β
π β
(0..^((β―βπ)
β 1))) |
33 | 31, 32 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
π β
(0..^((β―βπ)
β 1))) |
34 | | pfxtrcfv 14590 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ π β β
β§ π β (0..^((β―βπ) β 1))) β ((π prefix ((β―βπ) β 1))βπ) = (πβπ)) |
35 | 24, 26, 33, 34 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
((π prefix
((β―βπ) β
1))βπ) = (πβπ)) |
36 | 7 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (β―βπ) β
β0) |
37 | | elfzom1elp1fzo 13648 |
. . . . . . . . . . . . . . . . 17
β’
((((β―βπ)
β 1) β β€ β§ π β (0..^(((β―βπ) β 1) β 1))) β
(π + 1) β
(0..^((β―βπ)
β 1))) |
38 | 29, 37 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((β―βπ)
β β0 β§ π β (0..^(((β―βπ) β 1) β 1))) β
(π + 1) β
(0..^((β―βπ)
β 1))) |
39 | 36, 38 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
(π + 1) β
(0..^((β―βπ)
β 1))) |
40 | | pfxtrcfv 14590 |
. . . . . . . . . . . . . . 15
β’ ((π β Word π β§ π β β
β§ (π + 1) β (0..^((β―βπ) β 1))) β ((π prefix ((β―βπ) β 1))β(π + 1)) = (πβ(π + 1))) |
41 | 24, 26, 39, 40 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
((π prefix
((β―βπ) β
1))β(π + 1)) = (πβ(π + 1))) |
42 | 35, 41 | preq12d 4706 |
. . . . . . . . . . . . 13
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
{((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} = {(πβπ), (πβ(π + 1))}) |
43 | 42 | eleq1d 2819 |
. . . . . . . . . . . 12
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^(((β―βπ) β 1) β 1))) β
({((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β {(πβπ), (πβ(π + 1))} β ran πΈ)) |
44 | 43 | ex 414 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π β (0..^(((β―βπ) β 1) β 1)) β
({((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β {(πβπ), (πβ(π + 1))} β ran πΈ))) |
45 | 23, 44 | sylbid 239 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π β (0..^((β―β(π prefix ((β―βπ) β 1))) β 1))
β ({((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β {(πβπ), (πβ(π + 1))} β ran πΈ))) |
46 | 45 | imp 408 |
. . . . . . . . 9
β’ (((π β Word π β§ 2 β€ (β―βπ)) β§ π β (0..^((β―β(π prefix ((β―βπ) β 1))) β 1)))
β ({((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β {(πβπ), (πβ(π + 1))} β ran πΈ)) |
47 | 20, 46 | raleqbidva 3320 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ)) |
48 | | pfxtrcfvl 14594 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (lastSβ(π prefix ((β―βπ) β 1))) = (πβ((β―βπ) β 2))) |
49 | | pfxtrcfv0 14591 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((π prefix ((β―βπ) β 1))β0) = (πβ0)) |
50 | 48, 49 | preq12d 4706 |
. . . . . . . . 9
β’ ((π β Word π β§ 2 β€ (β―βπ)) β {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} =
{(πβ((β―βπ) β 2)), (πβ0)}) |
51 | 50 | eleq1d 2819 |
. . . . . . . 8
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ({(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ β {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) |
52 | 47, 51 | anbi12d 632 |
. . . . . . 7
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β ran πΈ) β (βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ))) |
53 | 52 | bicomd 222 |
. . . . . 6
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β (βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ))) |
54 | 53 | 3adant1 1131 |
. . . . 5
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β (βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ))) |
55 | | pfxcl 14574 |
. . . . . . 7
β’ (π β Word π β (π prefix ((β―βπ) β 1)) β Word π) |
56 | 55 | 3ad2ant2 1135 |
. . . . . 6
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (π prefix ((β―βπ) β 1)) β Word π) |
57 | 56 | 3biant1d 1479 |
. . . . 5
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β ran πΈ) β ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ))) |
58 | 54, 57 | bitrd 279 |
. . . 4
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((βπ β
(0..^((((β―βπ)
β 1) β 0) β 1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ) β ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ))) |
59 | 58 | anbi2d 630 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (βπ β (0..^((((β―βπ) β 1) β 0) β
1)){(πβπ), (πβ(π + 1))} β ran πΈ β§ {(πβ((β―βπ) β 2)), (πβ0)} β ran πΈ)) β ((lastSβπ) = (πβ0) β§ ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ)))) |
60 | 6, 59 | bitrd 279 |
. 2
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((lastSβπ) = (πβ0) β§ ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ)))) |
61 | | uspgrupgr 28176 |
. . . . . 6
β’ (πΊ β USPGraph β πΊ β
UPGraph) |
62 | | clwlkclwwlk.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
63 | 62, 1 | isclwlkupgr 28775 |
. . . . . . 7
β’ (πΊ β UPGraph β (π(ClWalksβπΊ)π β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ) β§ (βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπ)))))) |
64 | | 3an4anass 1106 |
. . . . . . 7
β’ (((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))) β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ) β§ (βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))} β§ (πβ0) = (πβ(β―βπ))))) |
65 | 63, 64 | bitr4di 289 |
. . . . . 6
β’ (πΊ β UPGraph β (π(ClWalksβπΊ)π β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
66 | 61, 65 | syl 17 |
. . . . 5
β’ (πΊ β USPGraph β (π(ClWalksβπΊ)π β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
67 | 66 | adantr 482 |
. . . 4
β’ ((πΊ β USPGraph β§ π β Word π) β (π(ClWalksβπΊ)π β ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
68 | 67 | exbidv 1925 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π) β (βπ π(ClWalksβπΊ)π β βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
69 | 68 | 3adant3 1133 |
. 2
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ π(ClWalksβπΊ)π β βπ((π β Word dom πΈ β§ π:(0...(β―βπ))βΆπ β§ βπ β (0..^(β―βπ))(πΈβ(πβπ)) = {(πβπ), (πβ(π + 1))}) β§ (πβ0) = (πβ(β―βπ))))) |
70 | | eqid 2733 |
. . . . . 6
β’
(EdgβπΊ) =
(EdgβπΊ) |
71 | 62, 70 | isclwwlk 28977 |
. . . . 5
β’ ((π prefix ((β―βπ) β 1)) β
(ClWWalksβπΊ) β
(((π prefix
((β―βπ) β
1)) β Word π β§
(π prefix
((β―βπ) β
1)) β β
) β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
(EdgβπΊ))) |
72 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β π β Word π) |
73 | | nn0ge2m1nn 12490 |
. . . . . . . . . . . 12
β’
(((β―βπ)
β β0 β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
β) |
74 | 7, 73 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β
β) |
75 | | nn0re 12430 |
. . . . . . . . . . . . . . 15
β’
((β―βπ)
β β0 β (β―βπ) β β) |
76 | 75 | lem1d 12096 |
. . . . . . . . . . . . . 14
β’
((β―βπ)
β β0 β ((β―βπ) β 1) β€ (β―βπ)) |
77 | 76 | a1d 25 |
. . . . . . . . . . . . 13
β’
((β―βπ)
β β0 β (2 β€ (β―βπ) β ((β―βπ) β 1) β€ (β―βπ))) |
78 | 7, 77 | syl 17 |
. . . . . . . . . . . 12
β’ (π β Word π β (2 β€ (β―βπ) β ((β―βπ) β 1) β€
(β―βπ))) |
79 | 78 | imp 408 |
. . . . . . . . . . 11
β’ ((π β Word π β§ 2 β€ (β―βπ)) β ((β―βπ) β 1) β€
(β―βπ)) |
80 | 72, 74, 79 | 3jca 1129 |
. . . . . . . . . 10
β’ ((π β Word π β§ 2 β€ (β―βπ)) β (π β Word π β§ ((β―βπ) β 1) β β β§
((β―βπ) β
1) β€ (β―βπ))) |
81 | 80 | 3adant1 1131 |
. . . . . . . . 9
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (π β Word π β§ ((β―βπ) β 1) β β β§
((β―βπ) β
1) β€ (β―βπ))) |
82 | | pfxn0 14583 |
. . . . . . . . 9
β’ ((π β Word π β§ ((β―βπ) β 1) β β β§
((β―βπ) β
1) β€ (β―βπ))
β (π prefix
((β―βπ) β
1)) β β
) |
83 | 81, 82 | syl 17 |
. . . . . . . 8
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (π prefix ((β―βπ) β 1)) β β
) |
84 | 83 | biantrud 533 |
. . . . . . 7
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((π prefix ((β―βπ) β 1)) β Word π β ((π prefix ((β―βπ) β 1)) β Word π β§ (π prefix ((β―βπ) β 1)) β
β
))) |
85 | 84 | bicomd 222 |
. . . . . 6
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (((π prefix ((β―βπ) β 1)) β Word π β§ (π prefix ((β―βπ) β 1)) β β
) β (π prefix ((β―βπ) β 1)) β Word π)) |
86 | 85 | 3anbi1d 1441 |
. . . . 5
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((((π prefix ((β―βπ) β 1)) β Word π β§ (π prefix ((β―βπ) β 1)) β β
) β§
βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
(EdgβπΊ)) β
((π prefix
((β―βπ) β
1)) β Word π β§
βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
(EdgβπΊ)))) |
87 | 71, 86 | bitrid 283 |
. . . 4
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((π prefix ((β―βπ) β 1)) β (ClWWalksβπΊ) β ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
(EdgβπΊ)))) |
88 | | biid 261 |
. . . . 5
β’ ((π prefix ((β―βπ) β 1)) β Word π β (π prefix ((β―βπ) β 1)) β Word π) |
89 | | edgval 28049 |
. . . . . . . 8
β’
(EdgβπΊ) = ran
(iEdgβπΊ) |
90 | 1 | eqcomi 2742 |
. . . . . . . . 9
β’
(iEdgβπΊ) =
πΈ |
91 | 90 | rneqi 5896 |
. . . . . . . 8
β’ ran
(iEdgβπΊ) = ran πΈ |
92 | 89, 91 | eqtri 2761 |
. . . . . . 7
β’
(EdgβπΊ) = ran
πΈ |
93 | 92 | eleq2i 2826 |
. . . . . 6
β’ ({((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β {((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ) |
94 | 93 | ralbii 3093 |
. . . . 5
β’
(βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ) |
95 | 92 | eleq2i 2826 |
. . . . 5
β’
({(lastSβ(π
prefix ((β―βπ)
β 1))), ((π prefix
((β―βπ) β
1))β0)} β (EdgβπΊ) β {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β ran πΈ) |
96 | 88, 94, 95 | 3anbi123i 1156 |
. . . 4
β’ (((π prefix ((β―βπ) β 1)) β Word π β§ βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
(EdgβπΊ)) β
((π prefix
((β―βπ) β
1)) β Word π β§
βπ β
(0..^((β―β(π
prefix ((β―βπ)
β 1))) β 1)){((π prefix ((β―βπ) β 1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β ran πΈ)) |
97 | 87, 96 | bitrdi 287 |
. . 3
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β ((π prefix ((β―βπ) β 1)) β (ClWWalksβπΊ) β ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ))) |
98 | 97 | anbi2d 630 |
. 2
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (((lastSβπ) = (πβ0) β§ (π prefix ((β―βπ) β 1)) β (ClWWalksβπΊ)) β ((lastSβπ) = (πβ0) β§ ((π prefix ((β―βπ) β 1)) β Word π β§ βπ β (0..^((β―β(π prefix ((β―βπ) β 1))) β
1)){((π prefix
((β―βπ) β
1))βπ), ((π prefix ((β―βπ) β 1))β(π + 1))} β ran πΈ β§ {(lastSβ(π prefix ((β―βπ) β 1))), ((π prefix ((β―βπ) β 1))β0)} β
ran πΈ)))) |
99 | 60, 69, 98 | 3bitr4d 311 |
1
β’ ((πΊ β USPGraph β§ π β Word π β§ 2 β€ (β―βπ)) β (βπ π(ClWalksβπΊ)π β ((lastSβπ) = (πβ0) β§ (π prefix ((β―βπ) β 1)) β (ClWWalksβπΊ)))) |