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

Proof

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

Metamath Proof Explorer

Theorem eupthvdres

Proof