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\upharpoonright }_{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\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩$$
7		opex	$$⊢⟨V,{I\upharpoonright }_{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\upharpoonright }_{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\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}\in \mathrm{V}$$
14	11 13	pm3.2i	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{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\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}\in \mathrm{V}\right)$$
16		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)=V$$
17	15 16	syl	$$⊢\phi \to \mathrm{Vtx}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)=V$$
18	10 17	eqtrid	$$⊢\phi \to \mathrm{Vtx}\left(H\right)=V$$
19	18 1	eqtrdi	$$⊢\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\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)$$
21		opiedgfv	$$⊢\left(V\in \mathrm{V}\wedge {I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}\in \mathrm{V}\right)\to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}$$
22	15 21	syl	$$⊢\phi \to \mathrm{iEdg}\left(⟨V,{I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}⟩\right)={I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}$$
23	20 22	eqtrid	$$⊢\phi \to \mathrm{iEdg}\left(H\right)={I\upharpoonright }_{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		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$$
26		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$$
27	5 24 25 26	4syl	$$⊢\phi \to F\left[\left(0..^\left|F\right|\right)\right]=\mathrm{dom}I$$
28	27	reseq2d	$$⊢\phi \to {I\upharpoonright }_{F\left[\left(0..^\left|F\right|\right)\right]}={I\upharpoonright }_{\mathrm{dom}I}$$
29	4	funfnd	$$⊢\phi \to IFn\mathrm{dom}I$$
30		fnresdm	$$⊢IFn\mathrm{dom}I\to {I\upharpoonright }_{\mathrm{dom}I}=I$$
31	29 30	syl	$$⊢\phi \to {I\upharpoonright }_{\mathrm{dom}I}=I$$
32	23 28 31	3eqtrd	$$⊢\phi \to \mathrm{iEdg}\left(H\right)=I$$
33	32 2	eqtrdi	$$⊢\phi \to \mathrm{iEdg}\left(H\right)=\mathrm{iEdg}\left(G\right)$$
34	3 9 19 33	vtxdeqd	$$⊢\phi \to \mathrm{VtxDeg}\left(H\right)=\mathrm{VtxDeg}\left(G\right)$$