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 
|- V = ( Vtx ` G )
finsumvtxdgeven.i 
|- I = ( iEdg ` G )
finsumvtxdgeven.d 
|- D = ( VtxDeg ` G )
Assertion finsumvtxdgeven 
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ v e. 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 e. Fin -> ( # ` I ) e. NN0 )
5 4 3ad2ant3 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( # ` I ) e. NN0 )
6 5 nn0zd 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( # ` I ) e. ZZ )
7 eqidd 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 x. ( # ` I ) ) = ( 2 x. ( # ` I ) ) )
8 2teven 
 |-  ( ( ( # ` I ) e. ZZ /\ ( 2 x. ( # ` I ) ) = ( 2 x. ( # ` I ) ) ) -> 2 || ( 2 x. ( # ` I ) ) )
9 6 7 8 syl2anc 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || ( 2 x. ( # ` I ) ) )
10 1 2 3 finsumvtxdg2size 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ v e. V ( D ` v ) = ( 2 x. ( # ` I ) ) )
11 9 10 breqtrrd 
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ v e. V ( D ` v ) )