Metamath Proof Explorer

Theorem wlk2v2e

Description: 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. 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)

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 wlk2v2e 
|- F ( Walks ` 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 1 opeq2i 
 |-  <. { X , Y } , I >. = <. { X , Y } , <" { X , Y } "> >.
8 6 7 eqtri 
 |-  G = <. { X , Y } , <" { X , Y } "> >.
9 uspgr2v1e2w 
 |-  ( ( X e. _V /\ Y e. _V ) -> <. { X , Y } , <" { X , Y } "> >. e. USPGraph )
10 3 4 9 mp2an 
 |-  <. { X , Y } , <" { X , Y } "> >. e. USPGraph
11 8 10 eqeltri 
 |-  G e. USPGraph
12 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
13 11 12 ax-mp 
 |-  G e. UPGraph
14 1 2 wlk2v2elem1 
 |-  F e. Word dom I
15 3 prid1 
 |-  X e. { X , Y }
16 4 prid2 
 |-  Y e. { X , Y }
17 s3cl 
 |-  ( ( X e. { X , Y } /\ Y e. { X , Y } /\ X e. { X , Y } ) -> <" X Y X "> e. Word { X , Y } )
18 15 16 15 17 mp3an 
 |-  <" X Y X "> e. Word { X , Y }
19 5 18 eqeltri 
 |-  P e. Word { X , Y }
20 wrdf 
 |-  ( P e. Word { X , Y } -> P : ( 0 ..^ ( # ` P ) ) --> { X , Y } )
21 19 20 ax-mp 
 |-  P : ( 0 ..^ ( # ` P ) ) --> { X , Y }
22 5 fveq2i 
 |-  ( # ` P ) = ( # ` <" X Y X "> )
23 s3len 
 |-  ( # ` <" X Y X "> ) = 3
24 22 23 eqtr2i 
 |-  3 = ( # ` P )
25 24 oveq2i 
 |-  ( 0 ..^ 3 ) = ( 0 ..^ ( # ` P ) )
26 25 feq2i 
 |-  ( P : ( 0 ..^ 3 ) --> { X , Y } <-> P : ( 0 ..^ ( # ` P ) ) --> { X , Y } )
27 21 26 mpbir 
 |-  P : ( 0 ..^ 3 ) --> { X , Y }
28 2 fveq2i 
 |-  ( # ` F ) = ( # ` <" 0 0 "> )
29 s2len 
 |-  ( # ` <" 0 0 "> ) = 2
30 28 29 eqtri 
 |-  ( # ` F ) = 2
31 30 oveq2i 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ... 2 )
32 3z 
 |-  3 e. ZZ
33 fzoval 
 |-  ( 3 e. ZZ -> ( 0 ..^ 3 ) = ( 0 ... ( 3 - 1 ) ) )
34 32 33 ax-mp 
 |-  ( 0 ..^ 3 ) = ( 0 ... ( 3 - 1 ) )
35 3m1e2 
 |-  ( 3 - 1 ) = 2
36 35 oveq2i 
 |-  ( 0 ... ( 3 - 1 ) ) = ( 0 ... 2 )
37 34 36 eqtr2i 
 |-  ( 0 ... 2 ) = ( 0 ..^ 3 )
38 31 37 eqtri 
 |-  ( 0 ... ( # ` F ) ) = ( 0 ..^ 3 )
39 38 feq2i 
 |-  ( P : ( 0 ... ( # ` F ) ) --> { X , Y } <-> P : ( 0 ..^ 3 ) --> { X , Y } )
40 27 39 mpbir 
 |-  P : ( 0 ... ( # ` F ) ) --> { X , Y }
41 1 2 3 4 5 wlk2v2elem2 
 |-  A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) }
42 14 40 41 3pm3.2i 
 |-  ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> { X , Y } /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } )
43 6 fveq2i 
 |-  ( Vtx ` G ) = ( Vtx ` <. { X , Y } , I >. )
44 prex 
 |-  { X , Y } e. _V
45 s1cli 
 |-  <" { X , Y } "> e. Word _V
46 1 45 eqeltri 
 |-  I e. Word _V
47 opvtxfv 
 |-  ( ( { X , Y } e. _V /\ I e. Word _V ) -> ( Vtx ` <. { X , Y } , I >. ) = { X , Y } )
48 44 46 47 mp2an 
 |-  ( Vtx ` <. { X , Y } , I >. ) = { X , Y }
49 43 48 eqtr2i 
 |-  { X , Y } = ( Vtx ` G )
50 6 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` <. { X , Y } , I >. )
51 opiedgfv 
 |-  ( ( { X , Y } e. _V /\ I e. Word _V ) -> ( iEdg ` <. { X , Y } , I >. ) = I )
52 44 46 51 mp2an 
 |-  ( iEdg ` <. { X , Y } , I >. ) = I
53 50 52 eqtr2i 
 |-  I = ( iEdg ` G )
54 49 53 upgriswlk 
 |-  ( G e. UPGraph -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> { X , Y } /\ A. k e. ( 0 ..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
55 42 54 mpbiri 
 |-  ( G e. UPGraph -> F ( Walks ` G ) P )
56 13 55 ax-mp 
 |-  F ( Walks ` G ) P