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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	sumvtxdg2size.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	sumvtxdg2size.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	fusgr1th	⊢ ( 𝐺 ∈ FinUSGraph → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sumvtxdg2size.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		sumvtxdg2size.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		sumvtxdg2size.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4	1 2	fusgrfupgrfs	⊢ ( 𝐺 ∈ FinUSGraph → ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) )
5	1 2 3	finsumvtxdg2size	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )
6	4 5	syl	⊢ ( 𝐺 ∈ FinUSGraph → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )