Metamath Proof Explorer


Theorem vtxdgoddnumeven

Description: The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in Diestel p. 5. See also remark about equation (2) in section I.1 in Bollobas p. 4. (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 vtxdgoddnumeven
|- ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || ( # ` { v e. V | -. 2 || ( 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 1 2 3 finsumvtxdgeven
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ w e. V ( D ` w ) )
5 incom
 |-  ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = ( { v e. V | 2 || ( D ` v ) } i^i { v e. V | -. 2 || ( D ` v ) } )
6 rabnc
 |-  ( { v e. V | 2 || ( D ` v ) } i^i { v e. V | -. 2 || ( D ` v ) } ) = (/)
7 5 6 eqtri
 |-  ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = (/)
8 7 a1i
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( { v e. V | -. 2 || ( D ` v ) } i^i { v e. V | 2 || ( D ` v ) } ) = (/) )
9 rabxm
 |-  V = ( { v e. V | 2 || ( D ` v ) } u. { v e. V | -. 2 || ( D ` v ) } )
10 9 equncomi
 |-  V = ( { v e. V | -. 2 || ( D ` v ) } u. { v e. V | 2 || ( D ` v ) } )
11 10 a1i
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> V = ( { v e. V | -. 2 || ( D ` v ) } u. { v e. V | 2 || ( D ` v ) } ) )
12 simp2
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> V e. Fin )
13 3 fveq1i
 |-  ( D ` w ) = ( ( VtxDeg ` G ) ` w )
14 dmfi
 |-  ( I e. Fin -> dom I e. Fin )
15 14 3ad2ant3
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> dom I e. Fin )
16 eqid
 |-  dom I = dom I
17 1 2 16 vtxdgfisnn0
 |-  ( ( dom I e. Fin /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 )
18 15 17 sylan
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 )
19 18 nn0cnd
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( ( VtxDeg ` G ) ` w ) e. CC )
20 13 19 eqeltrid
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. V ) -> ( D ` w ) e. CC )
21 8 11 12 20 fsumsplit
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. V ( D ` w ) = ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) )
22 21 breq2d
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || sum_ w e. V ( D ` w ) <-> 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) )
23 rabfi
 |-  ( V e. Fin -> { v e. V | -. 2 || ( D ` v ) } e. Fin )
24 23 3ad2ant2
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> { v e. V | -. 2 || ( D ` v ) } e. Fin )
25 elrabi
 |-  ( w e. { v e. V | -. 2 || ( D ` v ) } -> w e. V )
26 15 25 17 syl2an
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 )
27 26 nn0zd
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. ZZ )
28 13 27 eqeltrid
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> ( D ` w ) e. ZZ )
29 24 28 fsumzcl
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ )
30 29 adantr
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ )
31 fveq2
 |-  ( v = w -> ( D ` v ) = ( D ` w ) )
32 31 breq2d
 |-  ( v = w -> ( 2 || ( D ` v ) <-> 2 || ( D ` w ) ) )
33 32 notbid
 |-  ( v = w -> ( -. 2 || ( D ` v ) <-> -. 2 || ( D ` w ) ) )
34 33 elrab
 |-  ( w e. { v e. V | -. 2 || ( D ` v ) } <-> ( w e. V /\ -. 2 || ( D ` w ) ) )
35 34 simprbi
 |-  ( w e. { v e. V | -. 2 || ( D ` v ) } -> -. 2 || ( D ` w ) )
36 35 adantl
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | -. 2 || ( D ` v ) } ) -> -. 2 || ( D ` w ) )
37 24 28 36 sumodd
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) <-> 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) )
38 37 notbid
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) <-> -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) )
39 38 biimpa
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) )
40 rabfi
 |-  ( V e. Fin -> { v e. V | 2 || ( D ` v ) } e. Fin )
41 40 3ad2ant2
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> { v e. V | 2 || ( D ` v ) } e. Fin )
42 elrabi
 |-  ( w e. { v e. V | 2 || ( D ` v ) } -> w e. V )
43 15 42 17 syl2an
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. NN0 )
44 43 nn0zd
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( ( VtxDeg ` G ) ` w ) e. ZZ )
45 13 44 eqeltrid
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> ( D ` w ) e. ZZ )
46 41 45 fsumzcl
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ )
47 46 adantr
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ )
48 32 elrab
 |-  ( w e. { v e. V | 2 || ( D ` v ) } <-> ( w e. V /\ 2 || ( D ` w ) ) )
49 48 simprbi
 |-  ( w e. { v e. V | 2 || ( D ` v ) } -> 2 || ( D ` w ) )
50 49 adantl
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ w e. { v e. V | 2 || ( D ` v ) } ) -> 2 || ( D ` w ) )
51 41 45 50 sumeven
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) )
52 51 adantr
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) )
53 opeo
 |-  ( ( ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) e. ZZ /\ -. 2 || sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) ) /\ ( sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) e. ZZ /\ 2 || sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) )
54 30 39 47 52 53 syl22anc
 |-  ( ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) /\ -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) )
55 54 ex
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( -. 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) -> -. 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) ) )
56 55 con4d
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || ( sum_ w e. { v e. V | -. 2 || ( D ` v ) } ( D ` w ) + sum_ w e. { v e. V | 2 || ( D ` v ) } ( D ` w ) ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) )
57 22 56 sylbid
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> ( 2 || sum_ w e. V ( D ` w ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) ) )
58 4 57 mpd
 |-  ( ( G e. UPGraph /\ V e. Fin /\ I e. Fin ) -> 2 || ( # ` { v e. V | -. 2 || ( D ` v ) } ) )