This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupthvdres

Description: Formerly part of proof of eupth2 : The vertex degree remains the same for all vertices if the edges are restricted to the edges of an Eulerian path. (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypotheses eupthvdres.v 
|- V = ( Vtx ` G )
eupthvdres.i 
|- I = ( iEdg ` G )
eupthvdres.g 
|- ( ph -> G e. W )
eupthvdres.f 
|- ( ph -> Fun I )
eupthvdres.p 
|- ( ph -> F ( EulerPaths ` G ) P )
eupthvdres.h 
|- H = <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >.
Assertion eupthvdres 
|- ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) )

Proof

Step Hyp Ref Expression
1 eupthvdres.v 
 |-  V = ( Vtx ` G )
2 eupthvdres.i 
 |-  I = ( iEdg ` G )
3 eupthvdres.g 
 |-  ( ph -> G e. W )
4 eupthvdres.f 
 |-  ( ph -> Fun I )
5 eupthvdres.p 
 |-  ( ph -> F ( EulerPaths ` G ) P )
6 eupthvdres.h 
 |-  H = <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >.
7 opex 
 |-  <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. e. _V
8 6 7 eqeltri 
 |-  H e. _V
9 8 a1i 
 |-  ( ph -> H e. _V )
10 6 fveq2i 
 |-  ( Vtx ` H ) = ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. )
11 1 fvexi 
 |-  V e. _V
12 2 fvexi 
 |-  I e. _V
13 12 resex 
 |-  ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) e. _V
14 11 13 pm3.2i 
 |-  ( V e. _V /\ ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) e. _V )
15 14 a1i 
 |-  ( ph -> ( V e. _V /\ ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) e. _V ) )
16 opvtxfv 
 |-  ( ( V e. _V /\ ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) e. _V ) -> ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) = V )
17 15 16 syl 
 |-  ( ph -> ( Vtx ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) = V )
18 10 17 eqtrid 
 |-  ( ph -> ( Vtx ` H ) = V )
19 18 1 eqtrdi 
 |-  ( ph -> ( Vtx ` H ) = ( Vtx ` G ) )
20 6 fveq2i 
 |-  ( iEdg ` H ) = ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. )
21 opiedgfv 
 |-  ( ( V e. _V /\ ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) e. _V ) -> ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) = ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) )
22 15 21 syl 
 |-  ( ph -> ( iEdg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) = ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) )
23 20 22 eqtrid 
 |-  ( ph -> ( iEdg ` H ) = ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) )
24 2 eupthf1o 
 |-  ( F ( EulerPaths ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
25 f1ofo 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> F : ( 0 ..^ ( # ` F ) ) -onto-> dom I )
26 foima 
 |-  ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I -> ( F " ( 0 ..^ ( # ` F ) ) ) = dom I )
27 5 24 25 26 4syl 
 |-  ( ph -> ( F " ( 0 ..^ ( # ` F ) ) ) = dom I )
28 27 reseq2d 
 |-  ( ph -> ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) = ( I |` dom I ) )
29 4 funfnd 
 |-  ( ph -> I Fn dom I )
30 fnresdm 
 |-  ( I Fn dom I -> ( I |` dom I ) = I )
31 29 30 syl 
 |-  ( ph -> ( I |` dom I ) = I )
32 23 28 31 3eqtrd 
 |-  ( ph -> ( iEdg ` H ) = I )
33 32 2 eqtrdi 
 |-  ( ph -> ( iEdg ` H ) = ( iEdg ` G ) )
34 3 9 19 33 vtxdeqd 
 |-  ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) )