Metamath Proof Explorer


Theorem wlkf

Description: The mapping enumerating the (indices of the) edges of a walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021)

Ref Expression
Hypothesis wlkf.i 𝐼 = ( iEdg ‘ 𝐺 )
Assertion wlkf ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐹 ∈ Word dom 𝐼 )

Proof

Step Hyp Ref Expression
1 wlkf.i 𝐼 = ( iEdg ‘ 𝐺 )
2 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3 2 1 wlkprop ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 → ( 𝐹 ∈ Word dom 𝐼𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ ( Vtx ‘ 𝐺 ) ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) if- ( ( 𝑃𝑘 ) = ( 𝑃 ‘ ( 𝑘 + 1 ) ) , ( 𝐼 ‘ ( 𝐹𝑘 ) ) = { ( 𝑃𝑘 ) } , { ( 𝑃𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹𝑘 ) ) ) ) )
4 3 simp1d ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃𝐹 ∈ Word dom 𝐼 )