Metamath Proof Explorer

Theorem eulercrct

Description: A pseudograph with an Eulerian circuit <. F , P >. (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021)

Ref Expression
Hypothesis eulerpathpr.v 
|- V = ( Vtx ` G )
Assertion eulercrct 
|- ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> A. x e. V 2 || ( ( VtxDeg ` G ) ` x ) )

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 3adant3 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )
11 crctprop 
 |-  ( F ( Circuits ` G ) P -> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
12 11 simprd 
 |-  ( F ( Circuits ` G ) P -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
13 12 3ad2ant3 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
14 13 iftrued 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) = (/) )
15 14 eqeq2d 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) <-> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = (/) ) )
16 rabeq0 
 |-  ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = (/) <-> A. x e. V -. -. 2 || ( ( VtxDeg ` G ) ` x ) )
17 notnotr 
 |-  ( -. -. 2 || ( ( VtxDeg ` G ) ` x ) -> 2 || ( ( VtxDeg ` G ) ` x ) )
18 17 ralimi 
 |-  ( A. x e. V -. -. 2 || ( ( VtxDeg ` G ) ` x ) -> A. x e. V 2 || ( ( VtxDeg ` G ) ` x ) )
19 16 18 sylbi 
 |-  ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = (/) -> A. x e. V 2 || ( ( VtxDeg ` G ) ` x ) )
20 15 19 biimtrdi 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> ( { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) -> A. x e. V 2 || ( ( VtxDeg ` G ) ` x ) ) )
21 10 20 mpd 
 |-  ( ( G e. UPGraph /\ F ( EulerPaths ` G ) P /\ F ( Circuits ` G ) P ) -> A. x e. V 2 || ( ( VtxDeg ` G ) ` x ) )