This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( 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 eqtrid ⊢ ( 𝜑 → ( 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 eqtrid ⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) )
24 2 eupthf1o ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 )
25 f1ofo ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 → 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 )
26 foima ⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –onto→ dom 𝐼 → ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = dom 𝐼 )
27 5 24 25 26 4syl ⊢ ( 𝜑 → ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) = dom 𝐼 )
28 27 reseq2d ⊢ ( 𝜑 → ( 𝐼 ↾ ( 𝐹 “ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) ) = ( 𝐼 ↾ dom 𝐼 ) )
29 4 funfnd ⊢ ( 𝜑 → 𝐼 Fn dom 𝐼 )
30 fnresdm ⊢ ( 𝐼 Fn dom 𝐼 → ( 𝐼 ↾ dom 𝐼 ) = 𝐼 )
31 29 30 syl ⊢ ( 𝜑 → ( 𝐼 ↾ dom 𝐼 ) = 𝐼 )
32 23 28 31 3eqtrd ⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = 𝐼 )
33 32 2 eqtrdi ⊢ ( 𝜑 → ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐺 ) )
34 3 9 19 33 vtxdeqd ⊢ ( 𝜑 → ( VtxDeg ‘ 𝐻 ) = ( VtxDeg ‘ 𝐺 ) )