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 ) )