Step | Hyp | Ref
| Expression |
1 | | frgrhash2wsp.v |
. . . . . . 7
β’ π = (VtxβπΊ) |
2 | | fusgreg2wsp.m |
. . . . . . 7
β’ π = (π β π β¦ {π€ β (2 WSPathsN πΊ) β£ (π€β1) = π}) |
3 | 1, 2 | fusgr2wsp2nb 29320 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π£ β π) β (πβπ£) = βͺ π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) |
4 | 3 | fveq2d 6851 |
. . . . 5
β’ ((πΊ β FinUSGraph β§ π£ β π) β (β―β(πβπ£)) = (β―ββͺ π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©})) |
5 | 4 | adantr 482 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β (β―β(πβπ£)) = (β―ββͺ π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©})) |
6 | 1 | eleq2i 2830 |
. . . . . . 7
β’ (π£ β π β π£ β (VtxβπΊ)) |
7 | | nbfiusgrfi 28365 |
. . . . . . 7
β’ ((πΊ β FinUSGraph β§ π£ β (VtxβπΊ)) β (πΊ NeighbVtx π£) β Fin) |
8 | 6, 7 | sylan2b 595 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π£ β π) β (πΊ NeighbVtx π£) β Fin) |
9 | 8 | adantr 482 |
. . . . 5
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β (πΊ NeighbVtx π£) β Fin) |
10 | | eqid 2737 |
. . . . 5
β’ ((πΊ NeighbVtx π£) β {π}) = ((πΊ NeighbVtx π£) β {π}) |
11 | | snfi 8995 |
. . . . . 6
β’
{β¨βππ£πββ©} β Fin |
12 | 11 | a1i 11 |
. . . . 5
β’ ((((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β§ π β (πΊ NeighbVtx π£) β§ π β ((πΊ NeighbVtx π£) β {π})) β {β¨βππ£πββ©} β Fin) |
13 | 1 | nbgrssvtx 28332 |
. . . . . . . . . . 11
β’ (πΊ NeighbVtx π£) β π |
14 | 13 | a1i 11 |
. . . . . . . . . 10
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ π β (πΊ NeighbVtx π£)) β (πΊ NeighbVtx π£) β π) |
15 | 14 | ssdifd 4105 |
. . . . . . . . 9
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ π β (πΊ NeighbVtx π£)) β ((πΊ NeighbVtx π£) β {π}) β (π β {π})) |
16 | | iunss1 4973 |
. . . . . . . . 9
β’ (((πΊ NeighbVtx π£) β {π}) β (π β {π}) β βͺ
π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©} β βͺ π β (π β {π}){β¨βππ£πββ©}) |
17 | 15, 16 | syl 17 |
. . . . . . . 8
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ π β (πΊ NeighbVtx π£)) β βͺ
π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©} β βͺ π β (π β {π}){β¨βππ£πββ©}) |
18 | 17 | ralrimiva 3144 |
. . . . . . 7
β’ ((πΊ β FinUSGraph β§ π£ β π) β βπ β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©} β βͺ π β (π β {π}){β¨βππ£πββ©}) |
19 | | simpr 486 |
. . . . . . . 8
β’ ((πΊ β FinUSGraph β§ π£ β π) β π£ β π) |
20 | | s3iunsndisj 14860 |
. . . . . . . 8
β’ (π£ β π β Disj π β (πΊ NeighbVtx π£)βͺ π β (π β {π}){β¨βππ£πββ©}) |
21 | 19, 20 | syl 17 |
. . . . . . 7
β’ ((πΊ β FinUSGraph β§ π£ β π) β Disj π β (πΊ NeighbVtx π£)βͺ π β (π β {π}){β¨βππ£πββ©}) |
22 | | disjss2 5078 |
. . . . . . 7
β’
(βπ β
(πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©} β βͺ π β (π β {π}){β¨βππ£πββ©} β (Disj π β (πΊ NeighbVtx π£)βͺ π β (π β {π}){β¨βππ£πββ©} β Disj π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©})) |
23 | 18, 21, 22 | sylc 65 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π£ β π) β Disj π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) |
24 | 23 | adantr 482 |
. . . . 5
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β Disj π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) |
25 | 19 | adantr 482 |
. . . . . . 7
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β π£ β π) |
26 | 25 | anim1ci 617 |
. . . . . 6
β’ ((((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β§ π β (πΊ NeighbVtx π£)) β (π β (πΊ NeighbVtx π£) β§ π£ β π)) |
27 | | s3sndisj 14859 |
. . . . . 6
β’ ((π β (πΊ NeighbVtx π£) β§ π£ β π) β Disj π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) |
28 | 26, 27 | syl 17 |
. . . . 5
β’ ((((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β§ π β (πΊ NeighbVtx π£)) β Disj π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) |
29 | | s3cli 14777 |
. . . . . 6
β’
β¨βππ£πββ© β Word V |
30 | | hashsng 14276 |
. . . . . 6
β’
(β¨βππ£πββ© β Word V β
(β―β{β¨βππ£πββ©}) = 1) |
31 | 29, 30 | mp1i 13 |
. . . . 5
β’ ((((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β§ π β (πΊ NeighbVtx π£) β§ π β ((πΊ NeighbVtx π£) β {π})) β (β―β{β¨βππ£πββ©}) = 1) |
32 | 9, 10, 12, 24, 28, 31 | hash2iun1dif1 15716 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β (β―ββͺ π β (πΊ NeighbVtx π£)βͺ π β ((πΊ NeighbVtx π£) β {π}){β¨βππ£πββ©}) = ((β―β(πΊ NeighbVtx π£)) Β· ((β―β(πΊ NeighbVtx π£)) β 1))) |
33 | | fusgrusgr 28312 |
. . . . . . 7
β’ (πΊ β FinUSGraph β πΊ β
USGraph) |
34 | 1 | hashnbusgrvd 28518 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π£ β π) β (β―β(πΊ NeighbVtx π£)) = ((VtxDegβπΊ)βπ£)) |
35 | 33, 34 | sylan 581 |
. . . . . 6
β’ ((πΊ β FinUSGraph β§ π£ β π) β (β―β(πΊ NeighbVtx π£)) = ((VtxDegβπΊ)βπ£)) |
36 | | id 22 |
. . . . . . 7
β’
((β―β(πΊ
NeighbVtx π£)) =
((VtxDegβπΊ)βπ£) β (β―β(πΊ NeighbVtx π£)) = ((VtxDegβπΊ)βπ£)) |
37 | | oveq1 7369 |
. . . . . . 7
β’
((β―β(πΊ
NeighbVtx π£)) =
((VtxDegβπΊ)βπ£) β ((β―β(πΊ NeighbVtx π£)) β 1) = (((VtxDegβπΊ)βπ£) β 1)) |
38 | 36, 37 | oveq12d 7380 |
. . . . . 6
β’
((β―β(πΊ
NeighbVtx π£)) =
((VtxDegβπΊ)βπ£) β ((β―β(πΊ NeighbVtx π£)) Β· ((β―β(πΊ NeighbVtx π£)) β 1)) = (((VtxDegβπΊ)βπ£) Β· (((VtxDegβπΊ)βπ£) β 1))) |
39 | 35, 38 | syl 17 |
. . . . 5
β’ ((πΊ β FinUSGraph β§ π£ β π) β ((β―β(πΊ NeighbVtx π£)) Β· ((β―β(πΊ NeighbVtx π£)) β 1)) = (((VtxDegβπΊ)βπ£) Β· (((VtxDegβπΊ)βπ£) β 1))) |
40 | | id 22 |
. . . . . 6
β’
(((VtxDegβπΊ)βπ£) = πΎ β ((VtxDegβπΊ)βπ£) = πΎ) |
41 | | oveq1 7369 |
. . . . . 6
β’
(((VtxDegβπΊ)βπ£) = πΎ β (((VtxDegβπΊ)βπ£) β 1) = (πΎ β 1)) |
42 | 40, 41 | oveq12d 7380 |
. . . . 5
β’
(((VtxDegβπΊ)βπ£) = πΎ β (((VtxDegβπΊ)βπ£) Β· (((VtxDegβπΊ)βπ£) β 1)) = (πΎ Β· (πΎ β 1))) |
43 | 39, 42 | sylan9eq 2797 |
. . . 4
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β ((β―β(πΊ NeighbVtx π£)) Β· ((β―β(πΊ NeighbVtx π£)) β 1)) = (πΎ Β· (πΎ β 1))) |
44 | 5, 32, 43 | 3eqtrd 2781 |
. . 3
β’ (((πΊ β FinUSGraph β§ π£ β π) β§ ((VtxDegβπΊ)βπ£) = πΎ) β (β―β(πβπ£)) = (πΎ Β· (πΎ β 1))) |
45 | 44 | ex 414 |
. 2
β’ ((πΊ β FinUSGraph β§ π£ β π) β (((VtxDegβπΊ)βπ£) = πΎ β (β―β(πβπ£)) = (πΎ Β· (πΎ β 1)))) |
46 | 45 | ralrimiva 3144 |
1
β’ (πΊ β FinUSGraph β
βπ£ β π (((VtxDegβπΊ)βπ£) = πΎ β (β―β(πβπ£)) = (πΎ Β· (πΎ β 1)))) |