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

Metamath Proof Explorer

Theorem eupthseg

Description: The N -th edge in an eulerian path is the edge having P ( N ) and P ( N + 1 ) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 18-Feb-2021)

Ref Expression
Hypothesis eupths.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion eupthseg ( ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 eupths.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
2 1 eupthi ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1-onto→ dom 𝐼 ) )
3 2 simpld ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
4 1 wlkvtxeledg ⊢ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) )
5 fveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 𝑁 ) )
6 fvoveq1 ⊢ ( 𝑘 = 𝑁 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ ( 𝑁 + 1 ) ) )
7 5 6 preq12d ⊢ ( 𝑘 = 𝑁 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } )
8 2fveq3 ⊢ ( 𝑘 = 𝑁 → ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )
9 7 8 sseq12d ⊢ ( 𝑘 = 𝑁 → ( { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) ↔ { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
10 9 rspccv ⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
11 3 4 10 3syl ⊢ ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 → ( 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) → { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) ) )
12 11 imp ⊢ ( ( 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ) → { ( 𝑃 ‘ 𝑁 ) , ( 𝑃 ‘ ( 𝑁 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝑁 ) ) )