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 | |- I = ( iEdg ` G ) |
|
| Assertion | wlkf | |- ( F ( Walks ` G ) P -> F e. Word dom I ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkf.i | |- I = ( iEdg ` G ) |
|
| 2 | eqid | |- ( Vtx ` G ) = ( Vtx ` G ) |
|
| 3 | 2 1 | wlkprop | |- ( F ( Walks ` G ) P -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) |
| 4 | 3 | simp1d | |- ( F ( Walks ` G ) P -> F e. Word dom I ) |