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 𝐼 ) |
| 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 𝐼 ) |