Metamath Proof Explorer

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	$⊢ V = Vtx (G)$
		finsumvtxdgeven.i	$⊢ I = iEdg (G)$
		finsumvtxdgeven.d	$⊢ D = VtxDeg (G)$
	Assertion	finsumvtxdgeven	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \sum_{v \in V} D (v)$

Proof

Step	Hyp	Ref	Expression
1		finsumvtxdgeven.v	$⊢ V = Vtx (G)$
2		finsumvtxdgeven.i	$⊢ I = iEdg (G)$
3		finsumvtxdgeven.d	$⊢ D = VtxDeg (G)$
4		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
5	4	3ad2ant3	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \|I\| \in ℕ_{0}$
6	5	nn0zd	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \|I\| \in ℤ$
7		eqidd	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 \|I\| = 2 \|I\|$
8		2teven	$⊢ (\|I\| \in ℤ \land 2 \|I\| = 2 \|I\|) \to 2 ∥ 2 \|I\|$
9	6 7 8	syl2anc	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ 2 \|I\|$
10	1 2 3	finsumvtxdg2size	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to \sum_{v \in V} D (v) = 2 \|I\|$
11	9 10	breqtrrd	$⊢ (G \in UPGraph \land V \in Fin \land I \in Fin) \to 2 ∥ \sum_{v \in V} D (v)$