Metamath Proof Explorer


Theorem ntrl2v2e

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

Proof

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