Step | Hyp | Ref
| Expression |
1 | | clwwlkf1o.d |
. . 3
β’ π· = {π€ β (π WWalksN πΊ) β£ (lastSβπ€) = (π€β0)} |
2 | | clwwlkf1o.f |
. . 3
β’ πΉ = (π‘ β π· β¦ (π‘ prefix π)) |
3 | 1, 2 | clwwlkf 29040 |
. 2
β’ (π β β β πΉ:π·βΆ(π ClWWalksN πΊ)) |
4 | 1, 2 | clwwlkfv 29041 |
. . . . . 6
β’ (π₯ β π· β (πΉβπ₯) = (π₯ prefix π)) |
5 | 1, 2 | clwwlkfv 29041 |
. . . . . 6
β’ (π¦ β π· β (πΉβπ¦) = (π¦ prefix π)) |
6 | 4, 5 | eqeqan12d 2747 |
. . . . 5
β’ ((π₯ β π· β§ π¦ β π·) β ((πΉβπ₯) = (πΉβπ¦) β (π₯ prefix π) = (π¦ prefix π))) |
7 | 6 | adantl 483 |
. . . 4
β’ ((π β β β§ (π₯ β π· β§ π¦ β π·)) β ((πΉβπ₯) = (πΉβπ¦) β (π₯ prefix π) = (π¦ prefix π))) |
8 | | fveq2 6846 |
. . . . . . . . 9
β’ (π€ = π₯ β (lastSβπ€) = (lastSβπ₯)) |
9 | | fveq1 6845 |
. . . . . . . . 9
β’ (π€ = π₯ β (π€β0) = (π₯β0)) |
10 | 8, 9 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = π₯ β ((lastSβπ€) = (π€β0) β (lastSβπ₯) = (π₯β0))) |
11 | 10, 1 | elrab2 3652 |
. . . . . . 7
β’ (π₯ β π· β (π₯ β (π WWalksN πΊ) β§ (lastSβπ₯) = (π₯β0))) |
12 | | fveq2 6846 |
. . . . . . . . 9
β’ (π€ = π¦ β (lastSβπ€) = (lastSβπ¦)) |
13 | | fveq1 6845 |
. . . . . . . . 9
β’ (π€ = π¦ β (π€β0) = (π¦β0)) |
14 | 12, 13 | eqeq12d 2749 |
. . . . . . . 8
β’ (π€ = π¦ β ((lastSβπ€) = (π€β0) β (lastSβπ¦) = (π¦β0))) |
15 | 14, 1 | elrab2 3652 |
. . . . . . 7
β’ (π¦ β π· β (π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0))) |
16 | 11, 15 | anbi12i 628 |
. . . . . 6
β’ ((π₯ β π· β§ π¦ β π·) β ((π₯ β (π WWalksN πΊ) β§ (lastSβπ₯) = (π₯β0)) β§ (π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0)))) |
17 | | eqid 2733 |
. . . . . . . . . 10
β’
(VtxβπΊ) =
(VtxβπΊ) |
18 | | eqid 2733 |
. . . . . . . . . 10
β’
(EdgβπΊ) =
(EdgβπΊ) |
19 | 17, 18 | wwlknp 28837 |
. . . . . . . . 9
β’ (π₯ β (π WWalksN πΊ) β (π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1) β§ βπ β (0..^π){(π₯βπ), (π₯β(π + 1))} β (EdgβπΊ))) |
20 | 17, 18 | wwlknp 28837 |
. . . . . . . . . . . . 13
β’ (π¦ β (π WWalksN πΊ) β (π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1) β§ βπ β (0..^π){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ))) |
21 | | simprlr 779 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (β―βπ₯) = (π + 1)) |
22 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (β―βπ¦) = (π + 1)) |
23 | 21, 22 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (β―βπ₯) = (β―βπ¦)) |
24 | 23 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (β―βπ₯) = (β―βπ¦)) |
25 | | nncn 12169 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β β π β
β) |
26 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 1 β
β |
27 | | pncan 11415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
28 | 27 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β β β§ 1 β
β) β π = ((π + 1) β
1)) |
29 | 25, 26, 28 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π = ((π + 1) β 1)) |
30 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((β―βπ₯) =
(π + 1) β
((β―βπ₯) β
1) = ((π + 1) β
1)) |
31 | 30 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ₯) =
(π + 1) β ((π + 1) β 1) =
((β―βπ₯) β
1)) |
32 | 29, 31 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((β―βπ₯)
= (π + 1) β§ π β β) β π = ((β―βπ₯) β 1)) |
33 | 32 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ₯)
= (π + 1) β§ π β β) β (π₯ prefix π) = (π₯ prefix ((β―βπ₯) β 1))) |
34 | 32 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((β―βπ₯)
= (π + 1) β§ π β β) β (π¦ prefix π) = (π¦ prefix ((β―βπ₯) β 1))) |
35 | 33, 34 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((β―βπ₯)
= (π + 1) β§ π β β) β ((π₯ prefix π) = (π¦ prefix π) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1)))) |
36 | 35 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((β―βπ₯) =
(π + 1) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1))))) |
37 | 36 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1))))) |
38 | 37 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1))))) |
39 | 38 | impcom 409 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β ((π₯ prefix π) = (π¦ prefix π) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1)))) |
40 | 39 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1))) |
41 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β π¦ β Word (VtxβπΊ)) |
42 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β π₯ β Word (VtxβπΊ)) |
43 | 41, 42 | anim12ci 615 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ))) |
44 | 43 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β (π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ))) |
45 | | nnnn0 12428 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β π β
β0) |
46 | | 0nn0 12436 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
β0 |
47 | 45, 46 | jctil 521 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β (0 β
β0 β§ π
β β0)) |
48 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β (0 β
β0 β§ π
β β0)) |
49 | | nnre 12168 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β β π β
β) |
50 | 49 | lep1d 12094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β β π β€ (π + 1)) |
51 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ₯) =
(π + 1) β (π β€ (β―βπ₯) β π β€ (π + 1))) |
52 | 50, 51 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ₯) =
(π + 1) β (π β β β π β€ (β―βπ₯))) |
53 | 52 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β π β€ (β―βπ₯))) |
54 | 53 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (π β β β π β€ (β―βπ₯))) |
55 | 54 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β π β€ (β―βπ₯)) |
56 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((β―βπ¦) =
(π + 1) β (π β€ (β―βπ¦) β π β€ (π + 1))) |
57 | 50, 56 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((β―βπ¦) =
(π + 1) β (π β β β π β€ (β―βπ¦))) |
58 | 57 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β (π β β β π β€ (β―βπ¦))) |
59 | 58 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (π β β β π β€ (β―βπ¦))) |
60 | 59 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β π β€ (β―βπ¦)) |
61 | | pfxval 14570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π₯ β Word (VtxβπΊ) β§ π β β0) β (π₯ prefix π) = (π₯ substr β¨0, πβ©)) |
62 | 61 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0)) β (π₯ prefix π) = (π₯ substr β¨0, πβ©)) |
63 | | pfxval 14570 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π¦ β Word (VtxβπΊ) β§ π β β0) β (π¦ prefix π) = (π¦ substr β¨0, πβ©)) |
64 | 63 | ad2ant2l 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0)) β (π¦ prefix π) = (π¦ substr β¨0, πβ©)) |
65 | 62, 64 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0)) β ((π₯ prefix π) = (π¦ prefix π) β (π₯ substr β¨0, πβ©) = (π¦ substr β¨0, πβ©))) |
66 | 65 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0) β§ (π β€ (β―βπ₯) β§ π β€ (β―βπ¦))) β ((π₯ prefix π) = (π¦ prefix π) β (π₯ substr β¨0, πβ©) = (π¦ substr β¨0, πβ©))) |
67 | | swrdspsleq 14562 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0) β§ (π β€ (β―βπ₯) β§ π β€ (β―βπ¦))) β ((π₯ substr β¨0, πβ©) = (π¦ substr β¨0, πβ©) β βπ β (0..^π)(π₯βπ) = (π¦βπ))) |
68 | 66, 67 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ)) β§ (0 β β0 β§
π β
β0) β§ (π β€ (β―βπ₯) β§ π β€ (β―βπ¦))) β ((π₯ prefix π) = (π¦ prefix π) β βπ β (0..^π)(π₯βπ) = (π¦βπ))) |
69 | 44, 48, 55, 60, 68 | syl112anc 1375 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β ((π₯ prefix π) = (π¦ prefix π) β βπ β (0..^π)(π₯βπ) = (π¦βπ))) |
70 | | lbfzo0 13621 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 β
(0..^π) β π β
β) |
71 | 70 | biimpri 227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β β β 0 β
(0..^π)) |
72 | 71 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β 0 β (0..^π)) |
73 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β (π₯βπ) = (π₯β0)) |
74 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = 0 β (π¦βπ) = (π¦β0)) |
75 | 73, 74 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = 0 β ((π₯βπ) = (π¦βπ) β (π₯β0) = (π¦β0))) |
76 | 75 | rspcv 3579 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (0 β
(0..^π) β
(βπ β
(0..^π)(π₯βπ) = (π¦βπ) β (π₯β0) = (π¦β0))) |
77 | 72, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β (βπ β (0..^π)(π₯βπ) = (π¦βπ) β (π₯β0) = (π¦β0))) |
78 | 69, 77 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β ((π₯ prefix π) = (π¦ prefix π) β (π₯β0) = (π¦β0))) |
79 | 78 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (π₯β0) = (π¦β0)) |
80 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (lastSβπ₯) = (π₯β0)) |
81 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β (lastSβπ¦) = (π¦β0)) |
82 | 80, 81 | eqeqan12rd 2748 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β ((lastSβπ₯) = (lastSβπ¦) β (π₯β0) = (π¦β0))) |
83 | 82 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β ((lastSβπ₯) = (lastSβπ¦) β (π₯β0) = (π¦β0))) |
84 | 79, 83 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (lastSβπ₯) = (lastSβπ¦)) |
85 | 24, 40, 84 | jca32 517 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β ((β―βπ₯) = (β―βπ¦) β§ ((π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1)) β§ (lastSβπ₯) = (lastSβπ¦)))) |
86 | 42 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β π₯ β Word (VtxβπΊ)) |
87 | 86 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β π₯ β Word (VtxβπΊ)) |
88 | 41 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β π¦ β Word (VtxβπΊ)) |
89 | 88 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β π¦ β Word (VtxβπΊ)) |
90 | | 1red 11164 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β 1 β
β) |
91 | | nngt0 12192 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β 0 <
π) |
92 | | 0lt1 11685 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 <
1 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β β 0 <
1) |
94 | 49, 90, 91, 93 | addgt0d 11738 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β β β 0 <
(π + 1)) |
95 | | breq2 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ₯) =
(π + 1) β (0 <
(β―βπ₯) β 0
< (π +
1))) |
96 | 94, 95 | syl5ibr 246 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((β―βπ₯) =
(π + 1) β (π β β β 0 <
(β―βπ₯))) |
97 | 96 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β 0 <
(β―βπ₯))) |
98 | 97 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β (π β β β 0 <
(β―βπ₯))) |
99 | 98 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β 0 <
(β―βπ₯)) |
100 | 87, 89, 99 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β (π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ) β§ 0 < (β―βπ₯))) |
101 | 100 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ) β§ 0 < (β―βπ₯))) |
102 | | pfxsuff1eqwrdeq 14596 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π₯ β Word (VtxβπΊ) β§ π¦ β Word (VtxβπΊ) β§ 0 < (β―βπ₯)) β (π₯ = π¦ β ((β―βπ₯) = (β―βπ¦) β§ ((π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1)) β§ (lastSβπ₯) = (lastSβπ¦))))) |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β (π₯ = π¦ β ((β―βπ₯) = (β―βπ¦) β§ ((π₯ prefix ((β―βπ₯) β 1)) = (π¦ prefix ((β―βπ₯) β 1)) β§ (lastSβπ₯) = (lastSβπ¦))))) |
104 | 85, 103 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ (((π β β β§ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)))) β§ (π₯ prefix π) = (π¦ prefix π)) β π₯ = π¦) |
105 | 104 | exp31 421 |
. . . . . . . . . . . . . . . 16
β’ (π β β β ((((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β§ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0))) β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))) |
106 | 105 | expdcom 416 |
. . . . . . . . . . . . . . 15
β’ (((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β§ (lastSβπ¦) = (π¦β0)) β (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦)))) |
107 | 106 | ex 414 |
. . . . . . . . . . . . . 14
β’ ((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1)) β ((lastSβπ¦) = (π¦β0) β (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
108 | 107 | 3adant3 1133 |
. . . . . . . . . . . . 13
β’ ((π¦ β Word (VtxβπΊ) β§ (β―βπ¦) = (π + 1) β§ βπ β (0..^π){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ)) β ((lastSβπ¦) = (π¦β0) β (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
109 | 20, 108 | syl 17 |
. . . . . . . . . . . 12
β’ (π¦ β (π WWalksN πΊ) β ((lastSβπ¦) = (π¦β0) β (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
110 | 109 | imp 408 |
. . . . . . . . . . 11
β’ ((π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0)) β (((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β§ (lastSβπ₯) = (π₯β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦)))) |
111 | 110 | expdcom 416 |
. . . . . . . . . 10
β’ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1)) β ((lastSβπ₯) = (π₯β0) β ((π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
112 | 111 | 3adant3 1133 |
. . . . . . . . 9
β’ ((π₯ β Word (VtxβπΊ) β§ (β―βπ₯) = (π + 1) β§ βπ β (0..^π){(π₯βπ), (π₯β(π + 1))} β (EdgβπΊ)) β ((lastSβπ₯) = (π₯β0) β ((π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
113 | 19, 112 | syl 17 |
. . . . . . . 8
β’ (π₯ β (π WWalksN πΊ) β ((lastSβπ₯) = (π₯β0) β ((π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0)) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))))) |
114 | 113 | imp31 419 |
. . . . . . 7
β’ (((π₯ β (π WWalksN πΊ) β§ (lastSβπ₯) = (π₯β0)) β§ (π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0))) β (π β β β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))) |
115 | 114 | com12 32 |
. . . . . 6
β’ (π β β β (((π₯ β (π WWalksN πΊ) β§ (lastSβπ₯) = (π₯β0)) β§ (π¦ β (π WWalksN πΊ) β§ (lastSβπ¦) = (π¦β0))) β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))) |
116 | 16, 115 | biimtrid 241 |
. . . . 5
β’ (π β β β ((π₯ β π· β§ π¦ β π·) β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦))) |
117 | 116 | imp 408 |
. . . 4
β’ ((π β β β§ (π₯ β π· β§ π¦ β π·)) β ((π₯ prefix π) = (π¦ prefix π) β π₯ = π¦)) |
118 | 7, 117 | sylbid 239 |
. . 3
β’ ((π β β β§ (π₯ β π· β§ π¦ β π·)) β ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦)) |
119 | 118 | ralrimivva 3194 |
. 2
β’ (π β β β
βπ₯ β π· βπ¦ β π· ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦)) |
120 | | dff13 7206 |
. 2
β’ (πΉ:π·β1-1β(π ClWWalksN πΊ) β (πΉ:π·βΆ(π ClWWalksN πΊ) β§ βπ₯ β π· βπ¦ β π· ((πΉβπ₯) = (πΉβπ¦) β π₯ = π¦))) |
121 | 3, 119, 120 | sylanbrc 584 |
1
β’ (π β β β πΉ:π·β1-1β(π ClWWalksN πΊ)) |