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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	eupthvdres.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
	eupthvdres.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
	eupthvdres.f	⊢ ( 𝜑 → Fun 𝐼 )
	eupthvdres.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
	eupthvdres.h	⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩
Assertion	eupthvdres	⊢ ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( VtxDeg ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eupthvdres.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		eupthvdres.i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3		eupthvdres.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑊 )
4		eupthvdres.f	⊢ ( 𝜑 → Fun 𝐼 )
5		eupthvdres.p	⊢ ( 𝜑 → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 )
6		eupthvdres.h	⊢ 𝐻 = ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩
7		opex	⊢ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ∈ V
8	6 7	eqeltri	⊢ 𝐻 ∈ V
9	8	a1i	⊢ ( 𝜑 → 𝐻 ∈ V )
10	6	fveq2i	⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ )
11	1	fvexi	⊢ 𝑉 ∈ V
12	2	fvexi	⊢ 𝐼 ∈ V
13	12	resex	⊢ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∈ V
14	11 13	pm3.2i	⊢ ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∈ V )
15	14	a1i	⊢ ( 𝜑 → ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∈ V ) )
16		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) = 𝑉 )
17	15 16	syl	⊢ ( 𝜑 → ( Vtx ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) = 𝑉 )
18	10 17	syl5eq	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = 𝑉 )
19	18 1	eqtrdi	⊢ ( 𝜑 → ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐺 ) )
20	6	fveq2i	⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ )
21		opiedgfv	⊢ ( ( 𝑉 ∈ V ∧ ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
22	15 21	syl	⊢ ( 𝜑 → ( iEdg ‘ ⟨ 𝑉 , ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) ⟩ ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
23	20 22	syl5eq	⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
24	2	eupthf1o	⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 )
25	5 24	syl	⊢ ( 𝜑 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 )
26		f1ofo	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 )
27		foima	⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 → ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = dom 𝐼 )
28	25 26 27	3syl	⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = dom 𝐼 )
29	28	reseq2d	⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( 𝐼 ↾ dom 𝐼 ) )
30	4	funfnd	⊢ ( 𝜑 → 𝐼 Fn dom 𝐼 )
31		fnresdm	⊢ ( 𝐼 Fn dom 𝐼 → ( 𝐼 ↾ dom 𝐼 ) = 𝐼 )
32	30 31	syl	⊢ ( 𝜑 → ( 𝐼 ↾ dom 𝐼 ) = 𝐼 )
33	23 29 32	3eqtrd	⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = 𝐼 )
34	33 2	eqtrdi	⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
35	3 9 19 34	vtxdeqd	⊢ ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( VtxDeg ‘ 𝐺 ) )

Metamath Proof Explorer

Theorem eupthvdres

Proof