Step | Hyp | Ref
| Expression |
1 | | simpr2 1196 |
. . 3
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β π β π) |
2 | | simpr3 1197 |
. . 3
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β π β
β0) |
3 | | rusgrnumwwlk.v |
. . . . 5
β’ π = (VtxβπΊ) |
4 | | rusgrnumwwlk.l |
. . . . 5
β’ πΏ = (π£ β π, π β β0 β¦
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π£})) |
5 | 3, 4 | rusgrnumwwlklem 28957 |
. . . 4
β’ ((π β π β§ π β β0) β (ππΏπ) = (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π})) |
6 | 5 | eqeq1d 2739 |
. . 3
β’ ((π β π β§ π β β0) β ((ππΏπ) = (πΎβπ) β (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ))) |
7 | 1, 2, 6 | syl2anc 585 |
. 2
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β ((ππΏπ) = (πΎβπ) β (β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ))) |
8 | | eqid 2737 |
. . . . . . . . . . . . 13
β’
(EdgβπΊ) =
(EdgβπΊ) |
9 | 8 | wwlksnredwwlkn0 28883 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π€ β ((π + 1) WWalksN πΊ)) β ((π€β0) = π β βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)))) |
10 | 9 | ex 414 |
. . . . . . . . . . 11
β’ (π β β0
β (π€ β ((π + 1) WWalksN πΊ) β ((π€β0) = π β βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))))) |
11 | 10 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π β Fin β§ π β π β§ π β β0) β (π€ β ((π + 1) WWalksN πΊ) β ((π€β0) = π β βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))))) |
12 | 11 | adantl 483 |
. . . . . . . . 9
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (π€ β ((π + 1) WWalksN πΊ) β ((π€β0) = π β βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))))) |
13 | 12 | imp 408 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§ π€ β ((π + 1) WWalksN πΊ)) β ((π€β0) = π β βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)))) |
14 | 13 | rabbidva 3417 |
. . . . . . 7
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β {π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π} = {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
15 | 14 | adantr 482 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β {π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π} = {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
16 | 15 | fveq2d 6851 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π}) = (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
17 | | simp2 1138 |
. . . . . . . . . . . . 13
β’ (((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β (π¦β0) = π) |
18 | 17 | pm4.71ri 562 |
. . . . . . . . . . . 12
β’ (((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β ((π¦β0) = π β§ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)))) |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§ π€ β ((π + 1) WWalksN πΊ)) β§ π¦ β (π WWalksN πΊ)) β (((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β ((π¦β0) = π β§ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))))) |
20 | 19 | rexbidva 3174 |
. . . . . . . . . 10
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§ π€ β ((π + 1) WWalksN πΊ)) β (βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β βπ¦ β (π WWalksN πΊ)((π¦β0) = π β§ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))))) |
21 | | fveq1 6846 |
. . . . . . . . . . . 12
β’ (π₯ = π¦ β (π₯β0) = (π¦β0)) |
22 | 21 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π₯ = π¦ β ((π₯β0) = π β (π¦β0) = π)) |
23 | 22 | rexrab 3659 |
. . . . . . . . . 10
β’
(βπ¦ β
{π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β βπ¦ β (π WWalksN πΊ)((π¦β0) = π β§ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)))) |
24 | 20, 23 | bitr4di 289 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§ π€ β ((π + 1) WWalksN πΊ)) β (βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)) β βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ)))) |
25 | 24 | rabbidva 3417 |
. . . . . . . 8
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))} = {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
26 | 25 | adantr 482 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))} = {π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
27 | 26 | fveq2d 6851 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
28 | | simplr1 1216 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β π β Fin) |
29 | 3 | eleq1i 2829 |
. . . . . . . 8
β’ (π β Fin β
(VtxβπΊ) β
Fin) |
30 | 29 | biimpi 215 |
. . . . . . 7
β’ (π β Fin β
(VtxβπΊ) β
Fin) |
31 | | eqid 2737 |
. . . . . . . 8
β’ ((π + 1) WWalksN πΊ) = ((π + 1) WWalksN πΊ) |
32 | | eqid 2737 |
. . . . . . . 8
β’ {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} = {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} |
33 | 31, 8, 32 | hashwwlksnext 28901 |
. . . . . . 7
β’
((VtxβπΊ)
β Fin β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
34 | 28, 30, 33 | 3syl 18 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
35 | | fveq1 6846 |
. . . . . . . . . 10
β’ (π₯ = π€ β (π₯β0) = (π€β0)) |
36 | 35 | eqeq1d 2739 |
. . . . . . . . 9
β’ (π₯ = π€ β ((π₯β0) = π β (π€β0) = π)) |
37 | 36 | cbvrabv 3420 |
. . . . . . . 8
β’ {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
38 | 37 | sumeq1i 15590 |
. . . . . . 7
β’
Ξ£π¦ β
{π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
39 | 38 | a1i 11 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β Ξ£π¦ β {π₯ β (π WWalksN πΊ) β£ (π₯β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
40 | 27, 34, 39 | 3eqtrd 2781 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ βπ¦ β (π WWalksN πΊ)((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
41 | | rusgrnumwwlkslem 28956 |
. . . . . . . . . . 11
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))} = {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
42 | 41 | eqcomd 2743 |
. . . . . . . . . 10
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))} = {π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) |
43 | 42 | fveq2d 6851 |
. . . . . . . . 9
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
44 | 43 | adantl 483 |
. . . . . . . 8
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))})) |
45 | | elrabi 3644 |
. . . . . . . . . 10
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β π¦ β (π WWalksN πΊ)) |
46 | 45 | adantl 483 |
. . . . . . . . 9
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β π¦ β (π WWalksN πΊ)) |
47 | 3, 8 | wwlksnexthasheq 28890 |
. . . . . . . . 9
β’ (π¦ β (π WWalksN πΊ) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)})) |
48 | 46, 47 | syl 17 |
. . . . . . . 8
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)})) |
49 | 3 | rusgrpropadjvtx 28575 |
. . . . . . . . . 10
β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0*
β§ βπ β
π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ)) |
50 | | fveq1 6846 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ = π¦ β (π€β0) = (π¦β0)) |
51 | 50 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ = π¦ β ((π€β0) = π β (π¦β0) = π)) |
52 | 51 | elrab 3650 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β (π¦ β (π WWalksN πΊ) β§ (π¦β0) = π)) |
53 | 3, 8 | wwlknp 28830 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β (π WWalksN πΊ) β (π¦ β Word π β§ (β―βπ¦) = (π + 1) β§ βπ β (0..^π){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ))) |
54 | 53 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β (π WWalksN πΊ) β§ (π¦β0) = π) β (π¦ β Word π β§ (β―βπ¦) = (π + 1) β§ βπ β (0..^π){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ))) |
55 | | simpll 766 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β π¦ β Word π) |
56 | | nn0p1gt0 12449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β0
β 0 < (π +
1)) |
57 | 56 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β Fin β§ π β π β§ π β β0) β 0 <
(π + 1)) |
58 | 57 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β 0 <
(π + 1)) |
59 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((β―βπ¦) =
(π + 1) β (0 <
(β―βπ¦) β 0
< (π +
1))) |
60 | 59 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β (0 <
(β―βπ¦) β 0
< (π +
1))) |
61 | 58, 60 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β 0 <
(β―βπ¦)) |
62 | | hashle00 14307 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β Word π β ((β―βπ¦) β€ 0 β π¦ = β
)) |
63 | | lencl 14428 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π¦ β Word π β (β―βπ¦) β
β0) |
64 | 63 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π¦ β Word π β (β―βπ¦) β β) |
65 | | 0re 11164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
β |
66 | | lenlt 11240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((β―βπ¦)
β β β§ 0 β β) β ((β―βπ¦) β€ 0 β Β¬ 0 <
(β―βπ¦))) |
67 | 66 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((β―βπ¦)
β β β§ 0 β β) β (Β¬ 0 <
(β―βπ¦) β
(β―βπ¦) β€
0)) |
68 | 64, 65, 67 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β Word π β (Β¬ 0 < (β―βπ¦) β (β―βπ¦) β€ 0)) |
69 | | nne 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (Β¬
π¦ β β
β π¦ = β
) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β Word π β (Β¬ π¦ β β
β π¦ = β
)) |
71 | 62, 68, 70 | 3bitr4rd 312 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π¦ β Word π β (Β¬ π¦ β β
β Β¬ 0 <
(β―βπ¦))) |
72 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β (Β¬
π¦ β β
β Β¬
0 < (β―βπ¦))) |
73 | 72 | con4bid 317 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β (π¦ β β
β 0 <
(β―βπ¦))) |
74 | 61, 73 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β π¦ β β
) |
75 | 55, 74 | jca 513 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β§ (π β Fin β§ π β π β§ π β β0)) β (π¦ β Word π β§ π¦ β β
)) |
76 | 75 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β Word π β§ (β―βπ¦) = (π + 1)) β ((π β Fin β§ π β π β§ π β β0) β (π¦ β Word π β§ π¦ β β
))) |
77 | 76 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β Word π β§ (β―βπ¦) = (π + 1) β§ βπ β (0..^π){(π¦βπ), (π¦β(π + 1))} β (EdgβπΊ)) β ((π β Fin β§ π β π β§ π β β0) β (π¦ β Word π β§ π¦ β β
))) |
78 | 54, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β (π WWalksN πΊ) β§ (π¦β0) = π) β ((π β Fin β§ π β π β§ π β β0) β (π¦ β Word π β§ π¦ β β
))) |
79 | 52, 78 | sylbi 216 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β ((π β Fin β§ π β π β§ π β β0) β (π¦ β Word π β§ π¦ β β
))) |
80 | 79 | imp 408 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β§ (π β Fin β§ π β π β§ π β β0)) β (π¦ β Word π β§ π¦ β β
)) |
81 | | lswcl 14463 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β Word π β§ π¦ β β
) β (lastSβπ¦) β π) |
82 | 80, 81 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β§ (π β Fin β§ π β π β§ π β β0)) β
(lastSβπ¦) β
π) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ βπ β π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ) β (lastSβπ¦) β π) |
84 | | preq1 4699 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (lastSβπ¦) β {π, π} = {(lastSβπ¦), π}) |
85 | 84 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
β’ (π = (lastSβπ¦) β ({π, π} β (EdgβπΊ) β {(lastSβπ¦), π} β (EdgβπΊ))) |
86 | 85 | rabbidv 3418 |
. . . . . . . . . . . . . . . 16
β’ (π = (lastSβπ¦) β {π β π β£ {π, π} β (EdgβπΊ)} = {π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) |
87 | 86 | fveqeq2d 6855 |
. . . . . . . . . . . . . . 15
β’ (π = (lastSβπ¦) β ((β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ)) |
88 | 87 | rspcva 3582 |
. . . . . . . . . . . . . 14
β’
(((lastSβπ¦)
β π β§
βπ β π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ) β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ) |
89 | 83, 88 | sylancom 589 |
. . . . . . . . . . . . 13
β’ ((((π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ βπ β π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ) β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ) |
90 | 89 | exp41 436 |
. . . . . . . . . . . 12
β’ (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β ((π β Fin β§ π β π β§ π β β0) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β (βπ β π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ)))) |
91 | 90 | com14 96 |
. . . . . . . . . . 11
β’
(βπ β
π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ β ((π β Fin β§ π β π β§ π β β0) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ)))) |
92 | 91 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((πΊ β USGraph β§ πΎ β
β0* β§ βπ β π (β―β{π β π β£ {π, π} β (EdgβπΊ)}) = πΎ) β ((π β Fin β§ π β π β§ π β β0) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ)))) |
93 | 49, 92 | syl 17 |
. . . . . . . . 9
β’ (πΊ RegUSGraph πΎ β ((π β Fin β§ π β π β§ π β β0) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β (π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ)))) |
94 | 93 | imp41 427 |
. . . . . . . 8
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―β{π β π β£ {(lastSβπ¦), π} β (EdgβπΊ)}) = πΎ) |
95 | 44, 48, 94 | 3eqtrd 2781 |
. . . . . . 7
β’ ((((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β§ π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = πΎ) |
96 | 95 | sumeq2dv 15595 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}πΎ) |
97 | | oveq1 7369 |
. . . . . . . 8
β’
((β―β{π€
β (π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) Β· πΎ) = ((πΎβπ) Β· πΎ)) |
98 | 97 | adantl 483 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) Β· πΎ) = ((πΎβπ) Β· πΎ)) |
99 | | wwlksnfi 28893 |
. . . . . . . . . . . 12
β’
((VtxβπΊ)
β Fin β (π
WWalksN πΊ) β
Fin) |
100 | 29, 99 | sylbi 216 |
. . . . . . . . . . 11
β’ (π β Fin β (π WWalksN πΊ) β Fin) |
101 | 100 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π β Fin β§ π β π β§ π β β0) β (π WWalksN πΊ) β Fin) |
102 | 101 | ad2antlr 726 |
. . . . . . . . 9
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (π WWalksN πΊ) β Fin) |
103 | | rabfi 9220 |
. . . . . . . . 9
β’ ((π WWalksN πΊ) β Fin β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin) |
104 | 102, 103 | syl 17 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin) |
105 | | rusgrusgr 28554 |
. . . . . . . . . . . . 13
β’ (πΊ RegUSGraph πΎ β πΊ β USGraph) |
106 | | simp1 1137 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ π β π β§ π β β0) β π β Fin) |
107 | 105, 106 | anim12i 614 |
. . . . . . . . . . . 12
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (πΊ β USGraph β§ π β Fin)) |
108 | 3 | isfusgr 28308 |
. . . . . . . . . . . 12
β’ (πΊ β FinUSGraph β (πΊ β USGraph β§ π β Fin)) |
109 | 107, 108 | sylibr 233 |
. . . . . . . . . . 11
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β πΊ β
FinUSGraph) |
110 | | simpl 484 |
. . . . . . . . . . 11
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β πΊ RegUSGraph πΎ) |
111 | | ne0i 4299 |
. . . . . . . . . . . . 13
β’ (π β π β π β β
) |
112 | 111 | 3ad2ant2 1135 |
. . . . . . . . . . . 12
β’ ((π β Fin β§ π β π β§ π β β0) β π β β
) |
113 | 112 | adantl 483 |
. . . . . . . . . . 11
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β π β β
) |
114 | 3 | frusgrnn0 28561 |
. . . . . . . . . . 11
β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β
) β πΎ β
β0) |
115 | 109, 110,
113, 114 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β πΎ β
β0) |
116 | 115 | nn0cnd 12482 |
. . . . . . . . 9
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β πΎ β
β) |
117 | 116 | adantr 482 |
. . . . . . . 8
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β πΎ β β) |
118 | | fsumconst 15682 |
. . . . . . . 8
β’ (({π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin β§ πΎ β β) β Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}πΎ = ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) Β· πΎ)) |
119 | 104, 117,
118 | syl2anc 585 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}πΎ = ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) Β· πΎ)) |
120 | 116, 2 | expp1d 14059 |
. . . . . . . 8
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (πΎβ(π + 1)) = ((πΎβπ) Β· πΎ)) |
121 | 120 | adantr 482 |
. . . . . . 7
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (πΎβ(π + 1)) = ((πΎβπ) Β· πΎ)) |
122 | 98, 119, 121 | 3eqtr4d 2787 |
. . . . . 6
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}πΎ = (πΎβ(π + 1))) |
123 | 96, 122 | eqtrd 2777 |
. . . . 5
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β Ξ£π¦ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} (β―β{π€ β ((π + 1) WWalksN πΊ) β£ ((π€ prefix (π + 1)) = π¦ β§ (π¦β0) = π β§ {(lastSβπ¦), (lastSβπ€)} β (EdgβπΊ))}) = (πΎβ(π + 1))) |
124 | 16, 40, 123 | 3eqtrd 2781 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π}) = (πΎβ(π + 1))) |
125 | | peano2nn0 12460 |
. . . . . . . 8
β’ (π β β0
β (π + 1) β
β0) |
126 | 125 | 3ad2ant3 1136 |
. . . . . . 7
β’ ((π β Fin β§ π β π β§ π β β0) β (π + 1) β
β0) |
127 | 126 | adantl 483 |
. . . . . 6
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β (π + 1) β
β0) |
128 | 3, 4 | rusgrnumwwlklem 28957 |
. . . . . . 7
β’ ((π β π β§ (π + 1) β β0) β
(ππΏ(π + 1)) = (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π})) |
129 | 128 | eqeq1d 2739 |
. . . . . 6
β’ ((π β π β§ (π + 1) β β0) β
((ππΏ(π + 1)) = (πΎβ(π + 1)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π}) = (πΎβ(π + 1)))) |
130 | 1, 127, 129 | syl2anc 585 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β ((ππΏ(π + 1)) = (πΎβ(π + 1)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π}) = (πΎβ(π + 1)))) |
131 | 130 | adantr 482 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β ((ππΏ(π + 1)) = (πΎβ(π + 1)) β (β―β{π€ β ((π + 1) WWalksN πΊ) β£ (π€β0) = π}) = (πΎβ(π + 1)))) |
132 | 124, 131 | mpbird 257 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β§
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) β (ππΏ(π + 1)) = (πΎβ(π + 1))) |
133 | 132 | ex 414 |
. 2
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ) β (ππΏ(π + 1)) = (πΎβ(π + 1)))) |
134 | 7, 133 | sylbid 239 |
1
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β ((ππΏπ) = (πΎβπ) β (ππΏ(π + 1)) = (πΎβ(π + 1)))) |