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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
finsumvtxdgeven.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
finsumvtxdgeven.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxdgoddnumeven ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )

Proof

Step Hyp Ref Expression
1 finsumvtxdgeven.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 finsumvtxdgeven.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 finsumvtxdgeven.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4 1 2 3 finsumvtxdgeven ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ Σ 𝑤 ∈ 𝑉 ( 𝐷 ‘ 𝑤 ) )
5 incom ⊢ ( { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∩ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) = ( { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∩ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } )
6 rabnc ⊢ ( { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∩ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) = ∅
7 5 6 eqtri ⊢ ( { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∩ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) = ∅
8 7 a1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∩ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) = ∅ )
9 rabxm ⊢ 𝑉 = ( { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∪ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } )
10 9 equncomi ⊢ 𝑉 = ( { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∪ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } )
11 10 a1i ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 𝑉 = ( { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∪ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )
12 simp2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 𝑉 ∈ Fin )
13 3 fveq1i ⊢ ( 𝐷 ‘ 𝑤 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 )
14 dmfi ⊢ ( 𝐼 ∈ Fin → dom 𝐼 ∈ Fin )
15 14 3ad2ant3 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → dom 𝐼 ∈ Fin )
16 eqid ⊢ dom 𝐼 = dom 𝐼
17 1 2 16 vtxdgfisnn0 ⊢ ( ( dom 𝐼 ∈ Fin ∧ 𝑤 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℕ0 )
18 15 17 sylan ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℕ0 )
19 18 nn0cnd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℂ )
20 13 19 eqeltrid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ 𝑉 ) → ( 𝐷 ‘ 𝑤 ) ∈ ℂ )
21 8 11 12 20 fsumsplit ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑤 ∈ 𝑉 ( 𝐷 ‘ 𝑤 ) = ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) )
22 21 breq2d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 2 ∥ Σ 𝑤 ∈ 𝑉 ( 𝐷 ‘ 𝑤 ) ↔ 2 ∥ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) ) )
23 rabfi ⊢ ( 𝑉 ∈ Fin → { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∈ Fin )
24 23 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∈ Fin )
25 elrabi ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } → 𝑤 ∈ 𝑉 )
26 15 25 17 syl2an ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℕ0 )
27 26 nn0zd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℤ )
28 13 27 eqeltrid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
29 24 28 fsumzcl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
30 29 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) → Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
31 fveq2 ⊢ ( 𝑣 = 𝑤 → ( 𝐷 ‘ 𝑣 ) = ( 𝐷 ‘ 𝑤 ) )
32 31 breq2d ⊢ ( 𝑣 = 𝑤 → ( 2 ∥ ( 𝐷 ‘ 𝑣 ) ↔ 2 ∥ ( 𝐷 ‘ 𝑤 ) ) )
33 32 notbid ⊢ ( 𝑣 = 𝑤 → ( ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) ↔ ¬ 2 ∥ ( 𝐷 ‘ 𝑤 ) ) )
34 33 elrab ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ↔ ( 𝑤 ∈ 𝑉 ∧ ¬ 2 ∥ ( 𝐷 ‘ 𝑤 ) ) )
35 34 simprbi ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } → ¬ 2 ∥ ( 𝐷 ‘ 𝑤 ) )
36 35 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ¬ 2 ∥ ( 𝐷 ‘ 𝑤 ) )
37 24 28 36 sumodd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ↔ 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) )
38 37 notbid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ↔ ¬ 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) )
39 38 biimpa ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) → ¬ 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) )
40 rabfi ⊢ ( 𝑉 ∈ Fin → { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∈ Fin )
41 40 3ad2ant2 ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ∈ Fin )
42 elrabi ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } → 𝑤 ∈ 𝑉 )
43 15 42 17 syl2an ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℕ0 )
44 43 nn0zd ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑤 ) ∈ ℤ )
45 13 44 eqeltrid ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
46 41 45 fsumzcl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
47 46 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) → Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ )
48 32 elrab ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ↔ ( 𝑤 ∈ 𝑉 ∧ 2 ∥ ( 𝐷 ‘ 𝑤 ) ) )
49 48 simprbi ⊢ ( 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } → 2 ∥ ( 𝐷 ‘ 𝑤 ) )
50 49 adantl ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → 2 ∥ ( 𝐷 ‘ 𝑤 ) )
51 41 45 50 sumeven ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) )
52 51 adantr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) → 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) )
53 opeo ⊢ ( ( ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ ∧ ¬ 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) ∧ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ∈ ℤ ∧ 2 ∥ Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) ) → ¬ 2 ∥ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) )
54 30 39 47 52 53 syl22anc ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) ∧ ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) → ¬ 2 ∥ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) )
55 54 ex ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( ¬ 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) → ¬ 2 ∥ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) ) )
56 55 con4d ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 2 ∥ ( Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) + Σ 𝑤 ∈ { 𝑣 ∈ 𝑉 ∣ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ( 𝐷 ‘ 𝑤 ) ) → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) )
57 22 56 sylbid ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 2 ∥ Σ 𝑤 ∈ 𝑉 ( 𝐷 ‘ 𝑤 ) → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) ) )
58 4 57 mpd ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin ) → 2 ∥ ( ♯ ‘ { 𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ ( 𝐷 ‘ 𝑣 ) } ) )