Metamath Proof Explorer

Theorem fusgr1th

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 ∈ FinUSGraph → ∑ v ∈ V D ⁡ v = 2 ⁢ I

Proof

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 ∈ FinUSGraph → G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin
5 1 2 3 finsumvtxdg2size ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ∑ v ∈ V D ⁡ v = 2 ⁢ I
6 4 5 syl ⊢ G ∈ FinUSGraph → ∑ v ∈ V D ⁡ v = 2 ⁢ I