Step | Hyp | Ref
| Expression |
1 | | rusgrusgr 28554 |
. . . . 5
β’ (πΊ RegUSGraph πΎ β πΊ β USGraph) |
2 | 1 | ad2antlr 726 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΊ β
USGraph) |
3 | | simprl 770 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β π β π) |
4 | | simprr 772 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β π β
(β€β₯β3)) |
5 | | extwwlkfab.v |
. . . . 5
β’ π = (VtxβπΊ) |
6 | | extwwlkfab.c |
. . . . 5
β’ πΆ = (π£ β π, π β (β€β₯β2)
β¦ {π€ β (π£(ClWWalksNOnβπΊ)π) β£ (π€β(π β 2)) = π£}) |
7 | | extwwlkfab.f |
. . . . 5
β’ πΉ = (π(ClWWalksNOnβπΊ)(π β 2)) |
8 | 5, 6, 7 | numclwwlk1lem2 29346 |
. . . 4
β’ ((πΊ β USGraph β§ π β π β§ π β (β€β₯β3))
β (ππΆπ) β (πΉ Γ (πΊ NeighbVtx π))) |
9 | 2, 3, 4, 8 | syl3anc 1372 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (ππΆπ) β (πΉ Γ (πΊ NeighbVtx π))) |
10 | | hasheni 14255 |
. . 3
β’ ((ππΆπ) β (πΉ Γ (πΊ NeighbVtx π)) β (β―β(ππΆπ)) = (β―β(πΉ Γ (πΊ NeighbVtx π)))) |
11 | 9, 10 | syl 17 |
. 2
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―β(ππΆπ)) = (β―β(πΉ Γ (πΊ NeighbVtx π)))) |
12 | | eqid 2737 |
. . . . . . 7
β’
(VtxβπΊ) =
(VtxβπΊ) |
13 | 12 | clwwlknonfin 29080 |
. . . . . 6
β’
((VtxβπΊ)
β Fin β (π(ClWWalksNOnβπΊ)(π β 2)) β Fin) |
14 | 5 | eleq1i 2829 |
. . . . . 6
β’ (π β Fin β
(VtxβπΊ) β
Fin) |
15 | 7 | eleq1i 2829 |
. . . . . 6
β’ (πΉ β Fin β (π(ClWWalksNOnβπΊ)(π β 2)) β Fin) |
16 | 13, 14, 15 | 3imtr4i 292 |
. . . . 5
β’ (π β Fin β πΉ β Fin) |
17 | 16 | adantr 482 |
. . . 4
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β πΉ β Fin) |
18 | 17 | adantr 482 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΉ β
Fin) |
19 | 5 | finrusgrfusgr 28555 |
. . . . . . 7
β’ ((πΊ RegUSGraph πΎ β§ π β Fin) β πΊ β FinUSGraph) |
20 | 19 | ancoms 460 |
. . . . . 6
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β πΊ β FinUSGraph) |
21 | | fusgrfis 28320 |
. . . . . 6
β’ (πΊ β FinUSGraph β
(EdgβπΊ) β
Fin) |
22 | 20, 21 | syl 17 |
. . . . 5
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β (EdgβπΊ) β Fin) |
23 | 22 | adantr 482 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (EdgβπΊ) β
Fin) |
24 | | eqid 2737 |
. . . . 5
β’
(EdgβπΊ) =
(EdgβπΊ) |
25 | 5, 24 | nbusgrfi 28364 |
. . . 4
β’ ((πΊ β USGraph β§
(EdgβπΊ) β Fin
β§ π β π) β (πΊ NeighbVtx π) β Fin) |
26 | 2, 23, 3, 25 | syl3anc 1372 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (πΊ NeighbVtx π) β Fin) |
27 | | hashxp 14341 |
. . 3
β’ ((πΉ β Fin β§ (πΊ NeighbVtx π) β Fin) β (β―β(πΉ Γ (πΊ NeighbVtx π))) = ((β―βπΉ) Β· (β―β(πΊ NeighbVtx π)))) |
28 | 18, 26, 27 | syl2anc 585 |
. 2
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―β(πΉ
Γ (πΊ NeighbVtx π))) = ((β―βπΉ) Β· (β―β(πΊ NeighbVtx π)))) |
29 | 5 | rusgrpropnb 28573 |
. . . . . . . . 9
β’ (πΊ RegUSGraph πΎ β (πΊ β USGraph β§ πΎ β β0*
β§ βπ₯ β
π (β―β(πΊ NeighbVtx π₯)) = πΎ)) |
30 | | oveq2 7370 |
. . . . . . . . . . . 12
β’ (π₯ = π β (πΊ NeighbVtx π₯) = (πΊ NeighbVtx π)) |
31 | 30 | fveqeq2d 6855 |
. . . . . . . . . . 11
β’ (π₯ = π β ((β―β(πΊ NeighbVtx π₯)) = πΎ β (β―β(πΊ NeighbVtx π)) = πΎ)) |
32 | 31 | rspccv 3581 |
. . . . . . . . . 10
β’
(βπ₯ β
π (β―β(πΊ NeighbVtx π₯)) = πΎ β (π β π β (β―β(πΊ NeighbVtx π)) = πΎ)) |
33 | 32 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((πΊ β USGraph β§ πΎ β
β0* β§ βπ₯ β π (β―β(πΊ NeighbVtx π₯)) = πΎ) β (π β π β (β―β(πΊ NeighbVtx π)) = πΎ)) |
34 | 29, 33 | syl 17 |
. . . . . . . 8
β’ (πΊ RegUSGraph πΎ β (π β π β (β―β(πΊ NeighbVtx π)) = πΎ)) |
35 | 34 | adantl 483 |
. . . . . . 7
β’ ((π β Fin β§ πΊ RegUSGraph πΎ) β (π β π β (β―β(πΊ NeighbVtx π)) = πΎ)) |
36 | 35 | com12 32 |
. . . . . 6
β’ (π β π β ((π β Fin β§ πΊ RegUSGraph πΎ) β (β―β(πΊ NeighbVtx π)) = πΎ)) |
37 | 36 | adantr 482 |
. . . . 5
β’ ((π β π β§ π β (β€β₯β3))
β ((π β Fin β§
πΊ RegUSGraph πΎ) β (β―β(πΊ NeighbVtx π)) = πΎ)) |
38 | 37 | impcom 409 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―β(πΊ
NeighbVtx π)) = πΎ) |
39 | 38 | oveq2d 7378 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β ((β―βπΉ)
Β· (β―β(πΊ
NeighbVtx π))) =
((β―βπΉ) Β·
πΎ)) |
40 | | hashcl 14263 |
. . . . 5
β’ (πΉ β Fin β
(β―βπΉ) β
β0) |
41 | | nn0cn 12430 |
. . . . 5
β’
((β―βπΉ)
β β0 β (β―βπΉ) β β) |
42 | 18, 40, 41 | 3syl 18 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―βπΉ)
β β) |
43 | 20 | adantr 482 |
. . . . . 6
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΊ β
FinUSGraph) |
44 | | simplr 768 |
. . . . . 6
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΊ RegUSGraph πΎ) |
45 | | ne0i 4299 |
. . . . . . . 8
β’ (π β π β π β β
) |
46 | 45 | adantr 482 |
. . . . . . 7
β’ ((π β π β§ π β (β€β₯β3))
β π β
β
) |
47 | 46 | adantl 483 |
. . . . . 6
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β π β
β
) |
48 | 5 | frusgrnn0 28561 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ πΊ RegUSGraph πΎ β§ π β β
) β πΎ β
β0) |
49 | 43, 44, 47, 48 | syl3anc 1372 |
. . . . 5
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΎ β
β0) |
50 | 49 | nn0cnd 12482 |
. . . 4
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β πΎ β
β) |
51 | 42, 50 | mulcomd 11183 |
. . 3
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β ((β―βπΉ)
Β· πΎ) = (πΎ Β· (β―βπΉ))) |
52 | 39, 51 | eqtrd 2777 |
. 2
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β ((β―βπΉ)
Β· (β―β(πΊ
NeighbVtx π))) = (πΎ Β· (β―βπΉ))) |
53 | 11, 28, 52 | 3eqtrd 2781 |
1
β’ (((π β Fin β§ πΊ RegUSGraph πΎ) β§ (π β π β§ π β (β€β₯β3)))
β (β―β(ππΆπ)) = (πΎ Β· (β―βπΉ))) |