Description: A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e , but not a trail. Notice that G is a simple graph (without loops) only if X =/= Y . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021) (Proof shortened by AV, 30-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | wlk2v2e.i | |- I = <" { X , Y } "> |
|
| wlk2v2e.f | |- F = <" 0 0 "> |
||
| wlk2v2e.x | |- X e. _V |
||
| wlk2v2e.y | |- Y e. _V |
||
| wlk2v2e.p | |- P = <" X Y X "> |
||
| wlk2v2e.g | |- G = <. { X , Y } , I >. |
||
| Assertion | ntrl2v2e | |- -. F ( Trails ` G ) P |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wlk2v2e.i | |- I = <" { X , Y } "> |
|
| 2 | wlk2v2e.f | |- F = <" 0 0 "> |
|
| 3 | wlk2v2e.x | |- X e. _V |
|
| 4 | wlk2v2e.y | |- Y e. _V |
|
| 5 | wlk2v2e.p | |- P = <" X Y X "> |
|
| 6 | wlk2v2e.g | |- G = <. { X , Y } , I >. |
|
| 7 | 0z | |- 0 e. ZZ |
|
| 8 | 1z | |- 1 e. ZZ |
|
| 9 | 7 8 7 | 3pm3.2i | |- ( 0 e. ZZ /\ 1 e. ZZ /\ 0 e. ZZ ) |
| 10 | 0ne1 | |- 0 =/= 1 |
|
| 11 | s2prop | |- ( ( 0 e. ZZ /\ 0 e. ZZ ) -> <" 0 0 "> = { <. 0 , 0 >. , <. 1 , 0 >. } ) |
|
| 12 | 7 7 11 | mp2an | |- <" 0 0 "> = { <. 0 , 0 >. , <. 1 , 0 >. } |
| 13 | 2 12 | eqtri | |- F = { <. 0 , 0 >. , <. 1 , 0 >. } |
| 14 | 13 | fpropnf1 | |- ( ( ( 0 e. ZZ /\ 1 e. ZZ /\ 0 e. ZZ ) /\ 0 =/= 1 ) -> ( Fun F /\ -. Fun `' F ) ) |
| 15 | 9 10 14 | mp2an | |- ( Fun F /\ -. Fun `' F ) |
| 16 | 15 | simpri | |- -. Fun `' F |
| 17 | 16 | intnan | |- -. ( F ( Walks ` G ) P /\ Fun `' F ) |
| 18 | istrl | |- ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) ) |
|
| 19 | 17 18 | mtbir | |- -. F ( Trails ` G ) P |