# 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}=\mathrm{Vtx}\left({G}\right)$
eupthvdres.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
eupthvdres.g ${⊢}{\phi }\to {G}\in {W}$
eupthvdres.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
eupthvdres.p ${⊢}{\phi }\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
eupthvdres.h ${⊢}{H}=⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩$
Assertion eupthvdres ${⊢}{\phi }\to \mathrm{VtxDeg}\left({H}\right)=\mathrm{VtxDeg}\left({G}\right)$

### Proof

Step Hyp Ref Expression
1 eupthvdres.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 eupthvdres.i ${⊢}{I}=\mathrm{iEdg}\left({G}\right)$
3 eupthvdres.g ${⊢}{\phi }\to {G}\in {W}$
4 eupthvdres.f ${⊢}{\phi }\to \mathrm{Fun}{I}$
5 eupthvdres.p ${⊢}{\phi }\to {F}\mathrm{EulerPaths}\left({G}\right){P}$
6 eupthvdres.h ${⊢}{H}=⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩$
7 opex ${⊢}⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\in \mathrm{V}$
8 6 7 eqeltri ${⊢}{H}\in \mathrm{V}$
9 8 a1i ${⊢}{\phi }\to {H}\in \mathrm{V}$
10 6 fveq2i ${⊢}\mathrm{Vtx}\left({H}\right)=\mathrm{Vtx}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)$
11 1 fvexi ${⊢}{V}\in \mathrm{V}$
12 2 fvexi ${⊢}{I}\in \mathrm{V}$
13 12 resex ${⊢}{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}\in \mathrm{V}$
14 11 13 pm3.2i ${⊢}\left({V}\in \mathrm{V}\wedge {{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}\in \mathrm{V}\right)$
15 14 a1i ${⊢}{\phi }\to \left({V}\in \mathrm{V}\wedge {{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}\in \mathrm{V}\right)$
16 opvtxfv ${⊢}\left({V}\in \mathrm{V}\wedge {{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)={V}$
17 15 16 syl ${⊢}{\phi }\to \mathrm{Vtx}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)={V}$
18 10 17 syl5eq ${⊢}{\phi }\to \mathrm{Vtx}\left({H}\right)={V}$
19 18 1 syl6eq ${⊢}{\phi }\to \mathrm{Vtx}\left({H}\right)=\mathrm{Vtx}\left({G}\right)$
20 6 fveq2i ${⊢}\mathrm{iEdg}\left({H}\right)=\mathrm{iEdg}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)$
21 opiedgfv ${⊢}\left({V}\in \mathrm{V}\wedge {{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)={{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}$
22 15 21 syl ${⊢}{\phi }\to \mathrm{iEdg}\left(⟨{V},{{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}⟩\right)={{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}$
23 20 22 syl5eq ${⊢}{\phi }\to \mathrm{iEdg}\left({H}\right)={{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}$
24 2 eupthf1o ${⊢}{F}\mathrm{EulerPaths}\left({G}\right){P}\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1 onto}{⟶}\mathrm{dom}{I}$
25 5 24 syl ${⊢}{\phi }\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1 onto}{⟶}\mathrm{dom}{I}$
26 f1ofo ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1 onto}{⟶}\mathrm{dom}{I}\to {F}:\left(0..^\left|{F}\right|\right)\underset{onto}{⟶}\mathrm{dom}{I}$
27 foima ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{onto}{⟶}\mathrm{dom}{I}\to {F}\left[\left(0..^\left|{F}\right|\right)\right]=\mathrm{dom}{I}$
28 25 26 27 3syl ${⊢}{\phi }\to {F}\left[\left(0..^\left|{F}\right|\right)\right]=\mathrm{dom}{I}$
29 28 reseq2d ${⊢}{\phi }\to {{I}↾}_{{F}\left[\left(0..^\left|{F}\right|\right)\right]}={{I}↾}_{\mathrm{dom}{I}}$
30 4 funfnd ${⊢}{\phi }\to {I}Fn\mathrm{dom}{I}$
31 fnresdm ${⊢}{I}Fn\mathrm{dom}{I}\to {{I}↾}_{\mathrm{dom}{I}}={I}$
32 30 31 syl ${⊢}{\phi }\to {{I}↾}_{\mathrm{dom}{I}}={I}$
33 23 29 32 3eqtrd ${⊢}{\phi }\to \mathrm{iEdg}\left({H}\right)={I}$
34 33 2 syl6eq ${⊢}{\phi }\to \mathrm{iEdg}\left({H}\right)=\mathrm{iEdg}\left({G}\right)$
35 3 9 19 34 vtxdeqd ${⊢}{\phi }\to \mathrm{VtxDeg}\left({H}\right)=\mathrm{VtxDeg}\left({G}\right)$