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 e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )

Proof

Step Hyp Ref Expression
1 eulerpathpr.v 
 |-  V = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 simpl 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> G e. UPGraph )
4 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
5 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
6 4 5 syl 
 |-  ( G e. UPGraph -> Fun ( iEdg ` G ) )
7 6 adantr 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> Fun ( iEdg ` G ) )
8 simpr 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> F ( EulerPaths ` G ) P )
9 1 2 3 7 8 eupth2 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )
10 9 fveq2d 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) = ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) )
11 fveq2 
 |-  ( (/) = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) -> ( # ` (/) ) = ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) )
12 11 eleq1d 
 |-  ( (/) = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) -> ( ( # ` (/) ) e. { 0 , 2 } <-> ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) e. { 0 , 2 } ) )
13 fveq2 
 |-  ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) -> ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) = ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) )
14 13 eleq1d 
 |-  ( { ( P ` 0 ) , ( P ` ( # ` F ) ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) -> ( ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) e. { 0 , 2 } <-> ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) e. { 0 , 2 } ) )
15 hash0 
 |-  ( # ` (/) ) = 0
16 c0ex 
 |-  0 e. _V
17 16 prid1 
 |-  0 e. { 0 , 2 }
18 15 17 eqeltri 
 |-  ( # ` (/) ) e. { 0 , 2 }
19 18 a1i 
 |-  ( ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( # ` (/) ) e. { 0 , 2 } )
20 simpr 
 |-  ( ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) /\ -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> -. ( P ` 0 ) = ( P ` ( # ` F ) ) )
21 20 neqned 
 |-  ( ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) /\ -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
22 fvex 
 |-  ( P ` 0 ) e. _V
23 fvex 
 |-  ( P ` ( # ` F ) ) e. _V
24 hashprg 
 |-  ( ( ( P ` 0 ) e. _V /\ ( P ` ( # ` F ) ) e. _V ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) = 2 ) )
25 22 23 24 mp2an 
 |-  ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) = 2 )
26 21 25 sylib 
 |-  ( ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) /\ -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) = 2 )
27 2ex 
 |-  2 e. _V
28 27 prid2 
 |-  2 e. { 0 , 2 }
29 26 28 eqeltrdi 
 |-  ( ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) /\ -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( # ` { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) e. { 0 , 2 } )
30 12 14 19 29 ifbothda 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( # ` if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) e. { 0 , 2 } )
31 10 30 eqeltrd 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P ) -> ( # ` { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )