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 |