Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . 5
β’ (π€ = π‘ β (lastSβπ€) = (lastSβπ‘)) |
2 | | fveq1 6845 |
. . . . 5
β’ (π€ = π‘ β (π€β0) = (π‘β0)) |
3 | 1, 2 | eqeq12d 2749 |
. . . 4
β’ (π€ = π‘ β ((lastSβπ€) = (π€β0) β (lastSβπ‘) = (π‘β0))) |
4 | | clwwlkf1o.d |
. . . 4
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} |
5 | 3, 4 | elrab2 3652 |
. . 3
β’ (π‘ β π· β (π‘ β (π WWalksN πΊ) β§ (lastSβπ‘) = (π‘β0))) |
6 | | nnnn0 12428 |
. . . . . . . 8
β’ (π β β β π β
β0) |
7 | | iswwlksn 28832 |
. . . . . . . 8
β’ (π β β0
β (π‘ β (π WWalksN πΊ) β (π‘ β (WWalksβπΊ) β§ (β―βπ‘) = (π + 1)))) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’ (π β β β (π‘ β (π WWalksN πΊ) β (π‘ β (WWalksβπΊ) β§ (β―βπ‘) = (π + 1)))) |
9 | | eqid 2733 |
. . . . . . . . . 10
β’
(VtxβπΊ) =
(VtxβπΊ) |
10 | | eqid 2733 |
. . . . . . . . . 10
β’
(EdgβπΊ) =
(EdgβπΊ) |
11 | 9, 10 | iswwlks 28830 |
. . . . . . . . 9
β’ (π‘ β (WWalksβπΊ) β (π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ))) |
12 | 11 | a1i 11 |
. . . . . . . 8
β’ (π β β β (π‘ β (WWalksβπΊ) β (π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)))) |
13 | 12 | anbi1d 631 |
. . . . . . 7
β’ (π β β β ((π‘ β (WWalksβπΊ) β§ (β―βπ‘) = (π + 1)) β ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)))) |
14 | 8, 13 | bitrd 279 |
. . . . . 6
β’ (π β β β (π‘ β (π WWalksN πΊ) β ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)))) |
15 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β π‘ β Word (VtxβπΊ)) |
16 | | peano2nn0 12461 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β0
β (π + 1) β
β0) |
17 | 6, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β (π + 1) β
β0) |
18 | | nnre 12168 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β
β) |
19 | 18 | lep1d 12094 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β π β€ (π + 1)) |
20 | | elfz2nn0 13541 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...(π + 1)) β (π β β0 β§ (π + 1) β β0
β§ π β€ (π + 1))) |
21 | 6, 17, 19, 20 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β (0...(π + 1))) |
22 | 21 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β π β (0...(π + 1))) |
23 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ‘) =
(π + 1) β
(0...(β―βπ‘)) =
(0...(π +
1))) |
24 | 23 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
β’
((β―βπ‘) =
(π + 1) β (π β
(0...(β―βπ‘))
β π β (0...(π + 1)))) |
25 | 24 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β (π β (0...(β―βπ‘)) β π β (0...(π + 1)))) |
26 | 25 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β (π β (0...(β―βπ‘)) β π β (0...(π + 1)))) |
27 | 22, 26 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β π β (0...(β―βπ‘))) |
28 | 15, 27 | jca 513 |
. . . . . . . . . . . . 13
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β (π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘)))) |
29 | | pfxlen 14580 |
. . . . . . . . . . . . 13
β’ ((π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘))) β (β―β(π‘ prefix π)) = π) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
β’ (((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β§ π β β) β
(β―β(π‘ prefix
π)) = π) |
31 | 30 | ex 414 |
. . . . . . . . . . 11
β’ ((π‘ β Word (VtxβπΊ) β§ (β―βπ‘) = (π + 1)) β (π β β β (β―β(π‘ prefix π)) = π)) |
32 | 31 | 3ad2antl2 1187 |
. . . . . . . . . 10
β’ (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β (π β β β (β―β(π‘ prefix π)) = π)) |
33 | 32 | impcom 409 |
. . . . . . . . 9
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β (β―β(π‘ prefix π)) = π) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (β―β(π‘ prefix π)) = π) |
35 | | pfxcl 14574 |
. . . . . . . . . . . . 13
β’ (π‘ β Word (VtxβπΊ) β (π‘ prefix π) β Word (VtxβπΊ)) |
36 | 35 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β (π‘ prefix π) β Word (VtxβπΊ)) |
37 | 36 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β (π‘ prefix π) β Word (VtxβπΊ)) |
38 | 37 | ad2antrl 727 |
. . . . . . . . . 10
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β (π‘ prefix π) β Word (VtxβπΊ)) |
39 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ‘) =
(π + 1) β
((β―βπ‘) β
1) = ((π + 1) β
1)) |
40 | 39 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((β―βπ‘) =
(π + 1) β
(0..^((β―βπ‘)
β 1)) = (0..^((π + 1)
β 1))) |
41 | | nncn 12169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
β) |
42 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 1 β
β) |
43 | 41, 42 | pncand 11521 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β ((π + 1) β 1) = π) |
44 | 43 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β
(0..^((π + 1) β 1)) =
(0..^π)) |
45 | 40, 44 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β
(0..^((β―βπ‘)
β 1)) = (0..^π)) |
46 | 45 | raleqdv 3312 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ))) |
47 | | nnz 12528 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β π β
β€) |
48 | | peano2zm 12554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β€ β (π β 1) β
β€) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π β 1) β
β€) |
50 | 18 | lem1d 12096 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β (π β 1) β€ π) |
51 | | eluz2 12777 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
(β€β₯β(π β 1)) β ((π β 1) β β€ β§ π β β€ β§ (π β 1) β€ π)) |
52 | 49, 47, 50, 51 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β π β
(β€β₯β(π β 1))) |
53 | | fzoss2 13609 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(β€β₯β(π β 1)) β (0..^(π β 1)) β (0..^π)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β β β
(0..^(π β 1)) β
(0..^π)) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (0..^(π β 1)) β (0..^π)) |
56 | | ssralv 4014 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((0..^(π β 1))
β (0..^π) β
(βπ β
(0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ))) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ))) |
58 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β π‘ β Word (VtxβπΊ)) |
59 | 21 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β π β (0...(π + 1))) |
60 | 24 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (π β (0...(β―βπ‘)) β π β (0...(π + 1)))) |
61 | 59, 60 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β π β (0...(β―βπ‘))) |
62 | 61 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β π β (0...(β―βπ‘))) |
63 | 54 | sseld 3947 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β β β (π β (0..^(π β 1)) β π β (0..^π))) |
64 | 63 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β (π β (0..^(π β 1)) β π β (0..^π))) |
65 | 64 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β π β (0..^π)) |
66 | | pfxfv 14579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘)) β§ π β (0..^π)) β ((π‘ prefix π)βπ) = (π‘βπ)) |
67 | 66 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘)) β§ π β (0..^π)) β (π‘βπ) = ((π‘ prefix π)βπ)) |
68 | 58, 62, 65, 67 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β (π‘βπ) = ((π‘ prefix π)βπ)) |
69 | 47 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β π β β€) |
70 | | elfzom1elp1fzo 13648 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β€ β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
71 | 69, 70 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β (π + 1) β (0..^π)) |
72 | | pfxfv 14579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘)) β§ (π + 1) β (0..^π)) β ((π‘ prefix π)β(π + 1)) = (π‘β(π + 1))) |
73 | 72 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π‘ β Word (VtxβπΊ) β§ π β (0...(β―βπ‘)) β§ (π + 1) β (0..^π)) β (π‘β(π + 1)) = ((π‘ prefix π)β(π + 1))) |
74 | 58, 62, 71, 73 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β (π‘β(π + 1)) = ((π‘ prefix π)β(π + 1))) |
75 | 68, 74 | preq12d 4706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β {(π‘βπ), (π‘β(π + 1))} = {((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))}) |
76 | 75 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β§ π β (0..^(π β 1))) β ({(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))) |
77 | 76 | ralbidva 3169 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β (βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))) |
78 | 77 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β β β§
(β―βπ‘) = (π + 1)) β§ π‘ β Word (VtxβπΊ)) β (βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))) |
79 | 78 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (π‘ β Word (VtxβπΊ) β (βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
80 | 79 | com23 86 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (βπ β (0..^(π β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β (π‘ β Word (VtxβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
81 | 57, 80 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β (π‘ β Word (VtxβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
82 | 46, 81 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§
(β―βπ‘) = (π + 1)) β (βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β (π‘ β Word (VtxβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
83 | 82 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
((β―βπ‘) = (π + 1) β (βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β (π‘ β Word (VtxβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))))) |
84 | 83 | com23 86 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
(βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β ((β―βπ‘) = (π + 1) β (π‘ β Word (VtxβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))))) |
85 | 84 | com14 96 |
. . . . . . . . . . . . . . . 16
β’ (π‘ β Word (VtxβπΊ) β (βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β ((β―βπ‘) = (π + 1) β (π β β β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))))) |
86 | 85 | imp 408 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β ((β―βπ‘) = (π + 1) β (π β β β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
87 | 86 | 3adant1 1131 |
. . . . . . . . . . . . . 14
β’ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β ((β―βπ‘) = (π + 1) β (π β β β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)))) |
88 | 87 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β (π β β β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))) |
89 | 88 | impcom 409 |
. . . . . . . . . . . 12
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)) |
90 | 89 | ad2antrl 727 |
. . . . . . . . . . 11
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)) |
91 | | oveq1 7368 |
. . . . . . . . . . . . . 14
β’
((β―β(π‘
prefix π)) = π β ((β―β(π‘ prefix π)) β 1) = (π β 1)) |
92 | 91 | oveq2d 7377 |
. . . . . . . . . . . . 13
β’
((β―β(π‘
prefix π)) = π β
(0..^((β―β(π‘
prefix π)) β 1)) =
(0..^(π β
1))) |
93 | 92 | adantr 482 |
. . . . . . . . . . . 12
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β
(0..^((β―β(π‘
prefix π)) β 1)) =
(0..^(π β
1))) |
94 | 93 | raleqdv 3312 |
. . . . . . . . . . 11
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β (βπ β
(0..^((β―β(π‘
prefix π)) β
1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β βπ β (0..^(π β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ))) |
95 | 90, 94 | mpbird 257 |
. . . . . . . . . 10
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ)) |
96 | | simprl2 1220 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β π‘ β Word (VtxβπΊ)) |
97 | 19 | ancli 550 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β β β§ π β€ (π + 1))) |
98 | 47 | peano2zd 12618 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β β (π + 1) β
β€) |
99 | | fznn 13518 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π + 1) β β€ β
(π β (1...(π + 1)) β (π β β β§ π β€ (π + 1)))) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β (π β (1...(π + 1)) β (π β β β§ π β€ (π + 1)))) |
101 | 97, 100 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β π β (1...(π + 1))) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β π β (1...(π + 1))) |
103 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . 20
β’
((β―βπ‘) =
(π + 1) β
(1...(β―βπ‘)) =
(1...(π +
1))) |
104 | 103 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . 19
β’
((β―βπ‘) =
(π + 1) β (π β
(1...(β―βπ‘))
β π β (1...(π + 1)))) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β (π β (1...(β―βπ‘)) β π β (1...(π + 1)))) |
106 | 105 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β (π β (1...(β―βπ‘)) β π β (1...(π + 1)))) |
107 | 102, 106 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β π β (1...(β―βπ‘))) |
108 | 96, 107 | jca 513 |
. . . . . . . . . . . . . . 15
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β (π‘ β Word (VtxβπΊ) β§ π β (1...(β―βπ‘)))) |
109 | 108 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (π‘ β Word (VtxβπΊ) β§ π β (1...(β―βπ‘)))) |
110 | | pfxfvlsw 14592 |
. . . . . . . . . . . . . 14
β’ ((π‘ β Word (VtxβπΊ) β§ π β (1...(β―βπ‘))) β (lastSβ(π‘ prefix π)) = (π‘β(π β 1))) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (lastSβ(π‘ prefix π)) = (π‘β(π β 1))) |
112 | | pfxfv0 14589 |
. . . . . . . . . . . . . . 15
β’ ((π‘ β Word (VtxβπΊ) β§ π β (1...(β―βπ‘))) β ((π‘ prefix π)β0) = (π‘β0)) |
113 | 108, 112 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β ((π‘ prefix π)β0) = (π‘β0)) |
114 | 113 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β ((π‘ prefix π)β0) = (π‘β0)) |
115 | 111, 114 | preq12d 4706 |
. . . . . . . . . . . 12
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} = {(π‘β(π β 1)), (π‘β0)}) |
116 | | eqcom 2740 |
. . . . . . . . . . . . . . . . 17
β’
((lastSβπ‘) =
(π‘β0) β (π‘β0) = (lastSβπ‘)) |
117 | 116 | biimpi 215 |
. . . . . . . . . . . . . . . 16
β’
((lastSβπ‘) =
(π‘β0) β (π‘β0) = (lastSβπ‘)) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (π‘β0) = (lastSβπ‘)) |
119 | | lsw 14461 |
. . . . . . . . . . . . . . . . . 18
β’ (π‘ β Word (VtxβπΊ) β (lastSβπ‘) = (π‘β((β―βπ‘) β 1))) |
120 | 119 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . 17
β’ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β (lastSβπ‘) = (π‘β((β―βπ‘) β 1))) |
121 | 120 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β (lastSβπ‘) = (π‘β((β―βπ‘) β 1))) |
122 | 121 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (lastSβπ‘) = (π‘β((β―βπ‘) β 1))) |
123 | 39 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β ((β―βπ‘) β 1) = ((π + 1) β
1)) |
124 | 123, 43 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β ((β―βπ‘) β 1) = π) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β ((β―βπ‘) β 1) = π) |
126 | 125 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (π‘β((β―βπ‘) β 1)) = (π‘βπ)) |
127 | 118, 122,
126 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (π‘β0) = (π‘βπ)) |
128 | 127 | preq2d 4705 |
. . . . . . . . . . . . 13
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β {(π‘β(π β 1)), (π‘β0)} = {(π‘β(π β 1)), (π‘βπ)}) |
129 | 39, 43 | sylan9eq 2793 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((β―βπ‘)
= (π + 1) β§ π β β) β
((β―βπ‘) β
1) = π) |
130 | 129 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((β―βπ‘)
= (π + 1) β§ π β β) β
(0..^((β―βπ‘)
β 1)) = (0..^π)) |
131 | 130 | raleqdv 3312 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ‘)
= (π + 1) β§ π β β) β
(βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ))) |
132 | | fzo0end 13673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (π β 1) β (0..^π)) |
133 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (π β 1) β (π‘βπ) = (π‘β(π β 1))) |
134 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = (π β 1) β (π‘β(π + 1)) = (π‘β((π β 1) + 1))) |
135 | 133, 134 | preq12d 4706 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = (π β 1) β {(π‘βπ), (π‘β(π + 1))} = {(π‘β(π β 1)), (π‘β((π β 1) + 1))}) |
136 | 135 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = (π β 1) β ({(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ))) |
137 | 136 | rspcva 3581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β 1) β (0..^π) β§ βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β {(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ)) |
138 | 132, 137 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§
βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β {(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ)) |
139 | 41, 42 | npcand 11524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β β ((π β 1) + 1) = π) |
140 | 139 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β (π‘β((π β 1) + 1)) = (π‘βπ)) |
141 | 140 | preq2d 4705 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β {(π‘β(π β 1)), (π‘β((π β 1) + 1))} = {(π‘β(π β 1)), (π‘βπ)}) |
142 | 141 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β ({(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
143 | 142 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β ({(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
144 | 143 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§
βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β ({(π‘β(π β 1)), (π‘β((π β 1) + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
145 | 138, 144 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§
βπ β (0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)) |
146 | 145 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β
(βπ β
(0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
147 | 146 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((β―βπ‘)
= (π + 1) β§ π β β) β
(βπ β
(0..^π){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
148 | 131, 147 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
β’
(((β―βπ‘)
= (π + 1) β§ π β β) β
(βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
149 | 148 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’
((β―βπ‘) =
(π + 1) β (π β β β
(βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)))) |
150 | 149 | com3r 87 |
. . . . . . . . . . . . . . . . 17
β’
(βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ) β ((β―βπ‘) = (π + 1) β (π β β β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)))) |
151 | 150 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
β’ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β ((β―βπ‘) = (π + 1) β (π β β β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)))) |
152 | 151 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β (π β β β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ))) |
153 | 152 | impcom 409 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β {(π‘β(π β 1)), (π‘βπ)} β (EdgβπΊ)) |
155 | 128, 154 | eqeltrd 2834 |
. . . . . . . . . . . 12
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β {(π‘β(π β 1)), (π‘β0)} β (EdgβπΊ)) |
156 | 115, 155 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) |
157 | 156 | adantl 483 |
. . . . . . . . . 10
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) |
158 | 38, 95, 157 | 3jca 1129 |
. . . . . . . . 9
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β ((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ))) |
159 | | simpl 484 |
. . . . . . . . 9
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β (β―β(π‘ prefix π)) = π) |
160 | 158, 159 | jca 513 |
. . . . . . . 8
β’
(((β―β(π‘
prefix π)) = π β§ ((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β (0..^((β―βπ‘) β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0))) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π)) |
161 | 34, 160 | mpancom 687 |
. . . . . . 7
β’ (((π β β β§ ((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1))) β§ (lastSβπ‘) = (π‘β0)) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π)) |
162 | 161 | exp31 421 |
. . . . . 6
β’ (π β β β (((π‘ β β
β§ π‘ β Word (VtxβπΊ) β§ βπ β
(0..^((β―βπ‘)
β 1)){(π‘βπ), (π‘β(π + 1))} β (EdgβπΊ)) β§ (β―βπ‘) = (π + 1)) β ((lastSβπ‘) = (π‘β0) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π)))) |
163 | 14, 162 | sylbid 239 |
. . . . 5
β’ (π β β β (π‘ β (π WWalksN πΊ) β ((lastSβπ‘) = (π‘β0) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π)))) |
164 | 163 | imp32 420 |
. . . 4
β’ ((π β β β§ (π‘ β (π WWalksN πΊ) β§ (lastSβπ‘) = (π‘β0))) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π)) |
165 | 9, 10 | isclwwlknx 29029 |
. . . . 5
β’ (π β β β ((π‘ prefix π) β (π ClWWalksN πΊ) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π))) |
166 | 165 | adantr 482 |
. . . 4
β’ ((π β β β§ (π‘ β (π WWalksN πΊ) β§ (lastSβπ‘) = (π‘β0))) β ((π‘ prefix π) β (π ClWWalksN πΊ) β (((π‘ prefix π) β Word (VtxβπΊ) β§ βπ β (0..^((β―β(π‘ prefix π)) β 1)){((π‘ prefix π)βπ), ((π‘ prefix π)β(π + 1))} β (EdgβπΊ) β§ {(lastSβ(π‘ prefix π)), ((π‘ prefix π)β0)} β (EdgβπΊ)) β§ (β―β(π‘ prefix π)) = π))) |
167 | 164, 166 | mpbird 257 |
. . 3
β’ ((π β β β§ (π‘ β (π WWalksN πΊ) β§ (lastSβπ‘) = (π‘β0))) β (π‘ prefix π) β (π ClWWalksN πΊ)) |
168 | 5, 167 | sylan2b 595 |
. 2
β’ ((π β β β§ π‘ β π·) β (π‘ prefix π) β (π ClWWalksN πΊ)) |
169 | | clwwlkf1o.f |
. 2
β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) |
170 | 168, 169 | fmptd 7066 |
1
β’ (π β β β πΉ:π·βΆ(π ClWWalksN πΊ)) |