Description: The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 2-Jan-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wlkcomp.v | |- V = ( Vtx ` G ) |
|
| wlkcomp.i | |- I = ( iEdg ` G ) |
||
| wlkcomp.1 | |- F = ( 1st ` W ) |
||
| wlkcomp.2 | |- P = ( 2nd ` W ) |
||
| Assertion | wlkelwrd | |- ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlkcomp.v | |- V = ( Vtx ` G ) |
|
| 2 | wlkcomp.i | |- I = ( iEdg ` G ) |
|
| 3 | wlkcomp.1 | |- F = ( 1st ` W ) |
|
| 4 | wlkcomp.2 | |- P = ( 2nd ` W ) |
|
| 5 | 1 2 3 4 | wlkcompim | |- ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ 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 ) ) ) ) ) |
| 6 | 3simpa | |- ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ 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 ) ) ) ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) |
|
| 7 | 5 6 | syl | |- ( W e. ( Walks ` G ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) ) |