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 ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ v ∈ 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 ∈ Fin → I ∈ ℕ 0
5 4 3ad2ant3 ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → I ∈ ℕ 0
6 5 nn0zd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → I ∈ ℤ
7 eqidd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ⁢ I = 2 ⁢ I
8 2teven ⊢ I ∈ ℤ ∧ 2 ⁢ I = 2 ⁢ I → 2 ∥ 2 ⁢ I
9 6 7 8 syl2anc ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ 2 ⁢ I
10 1 2 3 finsumvtxdg2size ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → ∑ v ∈ V D ⁡ v = 2 ⁢ I
11 9 10 breqtrrd ⊢ G ∈ UPGraph ∧ V ∈ Fin ∧ I ∈ Fin → 2 ∥ ∑ v ∈ V D ⁡ v