Metamath Proof Explorer

Theorem eulerpathpr

Description: A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypothesis eulerpathpr.v ⊢V=Vtx⁡G
Assertion eulerpathpr ⊢G∈UPGraph∧FEulerPaths⁡GP→x∈V|¬2∥VtxDeg⁡G⁡x∈02

Proof

Step Hyp Ref Expression
1 eulerpathpr.v ⊢V=Vtx⁡G
2 eqid ⊢iEdg⁡G=iEdg⁡G
3 simpl ⊢G∈UPGraph∧FEulerPaths⁡GP→G∈UPGraph
4 upgruhgr ⊢G∈UPGraph→G∈UHGraph
5 2 uhgrfun ⊢G∈UHGraph→Fun⁡iEdg⁡G
6 4 5 syl ⊢G∈UPGraph→Fun⁡iEdg⁡G
7 6 adantr ⊢G∈UPGraph∧FEulerPaths⁡GP→Fun⁡iEdg⁡G
8 simpr ⊢G∈UPGraph∧FEulerPaths⁡GP→FEulerPaths⁡GP
9 1 2 3 7 8 eupth2 ⊢G∈UPGraph∧FEulerPaths⁡GP→x∈V|¬2∥VtxDeg⁡G⁡x=ifP⁡0=P⁡F∅P⁡0P⁡F
10 9 fveq2d ⊢G∈UPGraph∧FEulerPaths⁡GP→x∈V|¬2∥VtxDeg⁡G⁡x=ifP⁡0=P⁡F∅P⁡0P⁡F
11 fveq2 ⊢∅=ifP⁡0=P⁡F∅P⁡0P⁡F→∅=ifP⁡0=P⁡F∅P⁡0P⁡F
12 11 eleq1d ⊢∅=ifP⁡0=P⁡F∅P⁡0P⁡F→∅∈02↔ifP⁡0=P⁡F∅P⁡0P⁡F∈02
13 fveq2 ⊢P⁡0P⁡F=ifP⁡0=P⁡F∅P⁡0P⁡F→P⁡0P⁡F=ifP⁡0=P⁡F∅P⁡0P⁡F
14 13 eleq1d ⊢P⁡0P⁡F=ifP⁡0=P⁡F∅P⁡0P⁡F→P⁡0P⁡F∈02↔ifP⁡0=P⁡F∅P⁡0P⁡F∈02
15 hash0 ⊢∅=0
16 c0ex ⊢0∈V
17 16 prid1 ⊢0∈02
18 15 17 eqeltri ⊢∅∈02
19 18 a1i ⊢G∈UPGraph∧FEulerPaths⁡GP∧P⁡0=P⁡F→∅∈02
20 simpr ⊢G∈UPGraph∧FEulerPaths⁡GP∧¬P⁡0=P⁡F→¬P⁡0=P⁡F
21 20 neqned ⊢G∈UPGraph∧FEulerPaths⁡GP∧¬P⁡0=P⁡F→P⁡0≠P⁡F
22 fvex ⊢P⁡0∈V
23 fvex ⊢P⁡F∈V
24 hashprg ⊢P⁡0∈V∧P⁡F∈V→P⁡0≠P⁡F↔P⁡0P⁡F=2
25 22 23 24 mp2an ⊢P⁡0≠P⁡F↔P⁡0P⁡F=2
26 21 25 sylib ⊢G∈UPGraph∧FEulerPaths⁡GP∧¬P⁡0=P⁡F→P⁡0P⁡F=2
27 2ex ⊢2∈V
28 27 prid2 ⊢2∈02
29 26 28 eqeltrdi ⊢G∈UPGraph∧FEulerPaths⁡GP∧¬P⁡0=P⁡F→P⁡0P⁡F∈02
30 12 14 19 29 ifbothda ⊢G∈UPGraph∧FEulerPaths⁡GP→ifP⁡0=P⁡F∅P⁡0P⁡F∈02
31 10 30 eqeltrd ⊢G∈UPGraph∧FEulerPaths⁡GP→x∈V|¬2∥VtxDeg⁡G⁡x∈02