Step | Hyp | Ref
| Expression |
1 | | clwwlknclwwlkdif.a |
. . . . 5
β’ π΄ = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (lastSβπ€) β π)} |
2 | | clwwlknclwwlkdif.b |
. . . . 5
β’ π΅ = (π(π WWalksNOn πΊ)π) |
3 | | eqid 2733 |
. . . . 5
β’ {π€ β (π WWalksN πΊ) β£ (π€β0) = π} = {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
4 | 1, 2, 3 | clwwlknclwwlkdif 28972 |
. . . 4
β’ π΄ = ({π€ β (π WWalksN πΊ) β£ (π€β0) = π} β π΅) |
5 | 4 | fveq2i 6849 |
. . 3
β’
(β―βπ΄) =
(β―β({π€ β
(π WWalksN πΊ) β£ (π€β0) = π} β π΅)) |
6 | 5 | a1i 11 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
(β―βπ΄) =
(β―β({π€ β
(π WWalksN πΊ) β£ (π€β0) = π} β π΅))) |
7 | | clwwlknclwwlkdifnum.v |
. . . . . . . 8
β’ π = (VtxβπΊ) |
8 | 7 | eleq1i 2825 |
. . . . . . 7
β’ (π β Fin β
(VtxβπΊ) β
Fin) |
9 | 8 | biimpi 215 |
. . . . . 6
β’ (π β Fin β
(VtxβπΊ) β
Fin) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β (VtxβπΊ) β Fin) |
11 | 10 | adantr 482 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
(VtxβπΊ) β
Fin) |
12 | | wwlksnfi 28900 |
. . . 4
β’
((VtxβπΊ)
β Fin β (π
WWalksN πΊ) β
Fin) |
13 | | rabfi 9219 |
. . . 4
β’ ((π WWalksN πΊ) β Fin β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin) |
14 | 11, 12, 13 | 3syl 18 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin) |
15 | 7 | iswwlksnon 28847 |
. . . . . . . 8
β’ (π(π WWalksNOn πΊ)π) = {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} |
16 | | ancom 462 |
. . . . . . . . 9
β’ (((π€β0) = π β§ (π€βπ) = π) β ((π€βπ) = π β§ (π€β0) = π)) |
17 | 16 | rabbii 3412 |
. . . . . . . 8
β’ {π€ β (π WWalksN πΊ) β£ ((π€β0) = π β§ (π€βπ) = π)} = {π€ β (π WWalksN πΊ) β£ ((π€βπ) = π β§ (π€β0) = π)} |
18 | 15, 17 | eqtri 2761 |
. . . . . . 7
β’ (π(π WWalksNOn πΊ)π) = {π€ β (π WWalksN πΊ) β£ ((π€βπ) = π β§ (π€β0) = π)} |
19 | 18 | a1i 11 |
. . . . . 6
β’ ((π β π β§ π β β0) β (π(π WWalksNOn πΊ)π) = {π€ β (π WWalksN πΊ) β£ ((π€βπ) = π β§ (π€β0) = π)}) |
20 | 2, 19 | eqtrid 2785 |
. . . . 5
β’ ((π β π β§ π β β0) β π΅ = {π€ β (π WWalksN πΊ) β£ ((π€βπ) = π β§ (π€β0) = π)}) |
21 | | simpr 486 |
. . . . . . 7
β’ (((π€βπ) = π β§ (π€β0) = π) β (π€β0) = π) |
22 | 21 | a1i 11 |
. . . . . 6
β’ (π€ β (π WWalksN πΊ) β (((π€βπ) = π β§ (π€β0) = π) β (π€β0) = π)) |
23 | 22 | ss2rabi 4038 |
. . . . 5
β’ {π€ β (π WWalksN πΊ) β£ ((π€βπ) = π β§ (π€β0) = π)} β {π€ β (π WWalksN πΊ) β£ (π€β0) = π} |
24 | 20, 23 | eqsstrdi 4002 |
. . . 4
β’ ((π β π β§ π β β0) β π΅ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) |
25 | 24 | adantl 483 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β π΅ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) |
26 | | hashssdif 14321 |
. . 3
β’ (({π€ β (π WWalksN πΊ) β£ (π€β0) = π} β Fin β§ π΅ β {π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―β({π€ β (π WWalksN πΊ) β£ (π€β0) = π} β π΅)) = ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―βπ΅))) |
27 | 14, 25, 26 | syl2anc 585 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
(β―β({π€ β
(π WWalksN πΊ) β£ (π€β0) = π} β π΅)) = ((β―β{π€ β (π WWalksN πΊ) β£ (π€β0) = π}) β (β―βπ΅))) |
28 | | simpl 484 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ RegUSGraph πΎ) |
29 | 28 | adantr 482 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β πΊ RegUSGraph πΎ) |
30 | | simpr 486 |
. . . . 5
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β π β Fin) |
31 | 30 | adantr 482 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β π β Fin) |
32 | | simpl 484 |
. . . . 5
β’ ((π β π β§ π β β0) β π β π) |
33 | 32 | adantl 483 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β π β π) |
34 | | simpr 486 |
. . . . 5
β’ ((π β π β§ π β β0) β π β
β0) |
35 | 34 | adantl 483 |
. . . 4
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β π β
β0) |
36 | 7 | rusgrnumwwlkg 28970 |
. . . 4
β’ ((πΊ RegUSGraph πΎ β§ (π β Fin β§ π β π β§ π β β0)) β
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) |
37 | 29, 31, 33, 35, 36 | syl13anc 1373 |
. . 3
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
(β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) = (πΎβπ)) |
38 | 37 | oveq1d 7376 |
. 2
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
((β―β{π€ β
(π WWalksN πΊ) β£ (π€β0) = π}) β (β―βπ΅)) = ((πΎβπ) β (β―βπ΅))) |
39 | 6, 27, 38 | 3eqtrd 2777 |
1
β’ (((πΊ RegUSGraph πΎ β§ π β Fin) β§ (π β π β§ π β β0)) β
(β―βπ΄) = ((πΎβπ) β (β―βπ΅))) |