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