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	syl5eq	|- ( 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	syl5eq	|- ( ph -> ( iEdg ` H ) = ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) )
24	2	eupthf1o	|- ( F ( EulerPaths ` G ) P -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
25	5 24	syl	|- ( ph -> F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I )
26		f1ofo	|- ( F : ( 0 ..^ ( # ` F ) ) -1-1-onto-> dom I -> F : ( 0 ..^ ( # ` F ) ) -onto-> dom I )
27		foima	|- ( F : ( 0 ..^ ( # ` F ) ) -onto-> dom I -> ( F " ( 0 ..^ ( # ` F ) ) ) = dom I )
28	25 26 27	3syl	|- ( ph -> ( F " ( 0 ..^ ( # ` F ) ) ) = dom I )
29	28	reseq2d	|- ( ph -> ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) = ( I |` dom I ) )
30	4	funfnd	|- ( ph -> I Fn dom I )
31		fnresdm	|- ( I Fn dom I -> ( I |` dom I ) = I )
32	30 31	syl	|- ( ph -> ( I |` dom I ) = I )
33	23 29 32	3eqtrd	|- ( ph -> ( iEdg ` H ) = I )
34	33 2	eqtrdi	|- ( ph -> ( iEdg ` H ) = ( iEdg ` G ) )
35	3 9 19 34	vtxdeqd	|- ( ph -> ( VtxDeg ` H ) = ( VtxDeg ` G ) )