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