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 syl6bi
 |-  ( ( 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 ) )