| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cusgrusgr 28665 |
. . 3
β’ (πΊ β ComplUSGraph β
πΊ β
USGraph) |
| 2 | 1 | 3ad2ant1 1133 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β πΊ β
USGraph) |
| 3 | | hashnncl 14322 |
. . . . 5
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
| 4 | | nnm1nn0 12509 |
. . . . . 6
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0) |
| 5 | 4 | nn0xnn0d 12549 |
. . . . 5
β’
((β―βπ)
β β β ((β―βπ) β 1) β
β0*) |
| 6 | 3, 5 | syl6bir 253 |
. . . 4
β’ (π β Fin β (π β β
β
((β―βπ) β
1) β β0*)) |
| 7 | 6 | imp 407 |
. . 3
β’ ((π β Fin β§ π β β
) β
((β―βπ) β
1) β β0*) |
| 8 | 7 | 3adant1 1130 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β
((β―βπ) β
1) β β0*) |
| 9 | | cusgrcplgr 28666 |
. . . . . 6
β’ (πΊ β ComplUSGraph β
πΊ β
ComplGraph) |
| 10 | 9 | 3ad2ant1 1133 |
. . . . 5
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β πΊ β
ComplGraph) |
| 11 | | cusgrrusgr.v |
. . . . . 6
β’ π = (VtxβπΊ) |
| 12 | 11 | nbcplgr 28680 |
. . . . 5
β’ ((πΊ β ComplGraph β§ π£ β π) β (πΊ NeighbVtx π£) = (π β {π£})) |
| 13 | 10, 12 | sylan 580 |
. . . 4
β’ (((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β (πΊ NeighbVtx π£) = (π β {π£})) |
| 14 | 13 | ralrimiva 3146 |
. . 3
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β
βπ£ β π (πΊ NeighbVtx π£) = (π β {π£})) |
| 15 | 2 | anim1i 615 |
. . . . . . . 8
β’ (((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β (πΊ β USGraph β§ π£ β π)) |
| 16 | 15 | adantr 481 |
. . . . . . 7
β’ ((((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β§ (πΊ NeighbVtx π£) = (π β {π£})) β (πΊ β USGraph β§ π£ β π)) |
| 17 | 11 | hashnbusgrvd 28774 |
. . . . . . 7
β’ ((πΊ β USGraph β§ π£ β π) β (β―β(πΊ NeighbVtx π£)) = ((VtxDegβπΊ)βπ£)) |
| 18 | 16, 17 | syl 17 |
. . . . . 6
β’ ((((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β§ (πΊ NeighbVtx π£) = (π β {π£})) β (β―β(πΊ NeighbVtx π£)) = ((VtxDegβπΊ)βπ£)) |
| 19 | | fveq2 6888 |
. . . . . . 7
β’ ((πΊ NeighbVtx π£) = (π β {π£}) β (β―β(πΊ NeighbVtx π£)) = (β―β(π β {π£}))) |
| 20 | | hashdifsn 14370 |
. . . . . . . 8
β’ ((π β Fin β§ π£ β π) β (β―β(π β {π£})) = ((β―βπ) β 1)) |
| 21 | 20 | 3ad2antl2 1186 |
. . . . . . 7
β’ (((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β (β―β(π β {π£})) = ((β―βπ) β 1)) |
| 22 | 19, 21 | sylan9eqr 2794 |
. . . . . 6
β’ ((((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β§ (πΊ NeighbVtx π£) = (π β {π£})) β (β―β(πΊ NeighbVtx π£)) = ((β―βπ) β 1)) |
| 23 | 18, 22 | eqtr3d 2774 |
. . . . 5
β’ ((((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β§ (πΊ NeighbVtx π£) = (π β {π£})) β ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1)) |
| 24 | 23 | ex 413 |
. . . 4
β’ (((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β§ π£ β π) β ((πΊ NeighbVtx π£) = (π β {π£}) β ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1))) |
| 25 | 24 | ralimdva 3167 |
. . 3
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β
(βπ£ β π (πΊ NeighbVtx π£) = (π β {π£}) β βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1))) |
| 26 | 14, 25 | mpd 15 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β
βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1)) |
| 27 | | simp1 1136 |
. . 3
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β πΊ β
ComplUSGraph) |
| 28 | | ovex 7438 |
. . 3
β’
((β―βπ)
β 1) β V |
| 29 | | eqid 2732 |
. . . 4
β’
(VtxDegβπΊ) =
(VtxDegβπΊ) |
| 30 | 11, 29 | isrusgr0 28812 |
. . 3
β’ ((πΊ β ComplUSGraph β§
((β―βπ) β
1) β V) β (πΊ
RegUSGraph ((β―βπ) β 1) β (πΊ β USGraph β§ ((β―βπ) β 1) β
β0* β§ βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1)))) |
| 31 | 27, 28, 30 | sylancl 586 |
. 2
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β (πΊ RegUSGraph
((β―βπ) β
1) β (πΊ β USGraph
β§ ((β―βπ)
β 1) β β0* β§ βπ£ β π ((VtxDegβπΊ)βπ£) = ((β―βπ) β 1)))) |
| 32 | 2, 8, 26, 31 | mpbir3and 1342 |
1
β’ ((πΊ β ComplUSGraph β§ π β Fin β§ π β β
) β πΊ RegUSGraph
((β―βπ) β
1)) |
