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 φ G W
eupthvdres.f φ Fun I
eupthvdres.p φ F EulerPaths G P
eupthvdres.h H = V I F 0 ..^ F
Assertion eupthvdres φ VtxDeg H = VtxDeg G

Proof

Step Hyp Ref Expression
1 eupthvdres.v V = Vtx G
2 eupthvdres.i I = iEdg G
3 eupthvdres.g φ G W
4 eupthvdres.f φ Fun I
5 eupthvdres.p φ F EulerPaths G P
6 eupthvdres.h H = V I F 0 ..^ F
7 opex V I F 0 ..^ F V
8 6 7 eqeltri H V
9 8 a1i φ H V
10 6 fveq2i Vtx H = Vtx V I F 0 ..^ F
11 1 fvexi V V
12 2 fvexi I V
13 12 resex I F 0 ..^ F V
14 11 13 pm3.2i V V I F 0 ..^ F V
15 14 a1i φ V V I F 0 ..^ F V
16 opvtxfv V V I F 0 ..^ F V Vtx V I F 0 ..^ F = V
17 15 16 syl φ Vtx V I F 0 ..^ F = V
18 10 17 syl5eq φ Vtx H = V
19 18 1 syl6eq φ Vtx H = Vtx G
20 6 fveq2i iEdg H = iEdg V I F 0 ..^ F
21 opiedgfv V V I F 0 ..^ F V iEdg V I F 0 ..^ F = I F 0 ..^ F
22 15 21 syl φ iEdg V I F 0 ..^ F = I F 0 ..^ F
23 20 22 syl5eq φ 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 φ 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 φ F 0 ..^ F = dom I
29 28 reseq2d φ I F 0 ..^ F = I dom I
30 4 funfnd φ I Fn dom I
31 fnresdm I Fn dom I I dom I = I
32 30 31 syl φ I dom I = I
33 23 29 32 3eqtrd φ iEdg H = I
34 33 2 syl6eq φ iEdg H = iEdg G
35 3 9 19 34 vtxdeqd φ VtxDeg H = VtxDeg G