Description: The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in Bollobas p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory ). (Contributed by AV, 26-Dec-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | sumvtxdg2size.v | |- V = ( Vtx ` G ) |
|
| sumvtxdg2size.i | |- I = ( iEdg ` G ) |
||
| sumvtxdg2size.d | |- D = ( VtxDeg ` G ) |
||
| Assertion | fusgr1th | |- ( G e. FinUSGraph -> sum_ v e. V ( D ` v ) = ( 2 x. ( # ` I ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sumvtxdg2size.v | |- V = ( Vtx ` G ) |
|
| 2 | sumvtxdg2size.i | |- I = ( iEdg ` G ) |
|
| 3 | sumvtxdg2size.d | |- D = ( VtxDeg ` G ) |
|
| 4 | 1 2 | fusgrfupgrfs | |- ( G e. FinUSGraph -> ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) ) |
| 5 | 1 2 3 | finsumvtxdg2size | |- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ v e. V ( D ` v ) = ( 2 x. ( # ` I ) ) ) |
| 6 | 4 5 | syl | |- ( G e. FinUSGraph -> sum_ v e. V ( D ` v ) = ( 2 x. ( # ` I ) ) ) |