This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( 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 ∥ Σ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) )