Theorem finsumvtxdgeven

Description: The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in Bollobas p. 4, where it is also called thehandshaking lemma. (Contributed by AV, 22-Dec-2021)

	Ref	Expression
Hypotheses	finsumvtxdgeven.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	finsumvtxdgeven.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	finsumvtxdgeven.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion	finsumvtxdgeven	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) )

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdgeven.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		finsumvtxdgeven.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		finsumvtxdgeven.d	⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4		hashcl	⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
5	4	3ad2ant3	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
6	5	nn0zd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( ♯ ‘ 𝐼 ) ∈ ℤ )
7		eqidd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 2 · ( ♯ ‘ 𝐼 ) ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )
8		2teven	⊢ ( ( ( ♯ ‘ 𝐼 ) ∈ ℤ ∧ ( 2 · ( ♯ ‘ 𝐼 ) ) = ( 2 · ( ♯ ‘ 𝐼 ) ) ) → 2 ∥ ( 2 · ( ♯ ‘ 𝐼 ) ) )
9	6 7 8	syl2anc	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ ( 2 · ( ♯ ‘ 𝐼 ) ) )
10	1 2 3	finsumvtxdg2size	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = ( 2 · ( ♯ ‘ 𝐼 ) ) )
11	9 10	breqtrrd	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) )