MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clwwlk Structured version   Unicode version

Definition df-clwwlk 25321
Description: Define the set of all Closed Walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined in df-clwlk 25320. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk.

Notice that by this definition, a single vertex cannot be represented as closed walk, since the word <" v "> with vertex v represents the walk "vv", which is a (closed) walk of length 1 (if there is an edge/loop from v to v). Therefore, a closed walk corresponds to a closed walk as word in an undirected graph only for walks of length at least 1, see clwlkisclwwlk2 25360. (Contributed by Alexander van der Vekens, 20-Mar-2018.)

Assertion
Ref Expression
df-clwwlk  |- ClWWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
Distinct variable group:    e, i, v, w

Detailed syntax breakdown of Definition df-clwwlk
StepHypRef Expression
1 cclwwlk 25318 . 2  class ClWWalks
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3078 . . 3  class  _V
5 vi . . . . . . . . . 10  setvar  i
65cv 1436 . . . . . . . . 9  class  i
7 vw . . . . . . . . . 10  setvar  w
87cv 1436 . . . . . . . . 9  class  w
96, 8cfv 5592 . . . . . . . 8  class  ( w `
 i )
10 c1 9529 . . . . . . . . . 10  class  1
11 caddc 9531 . . . . . . . . . 10  class  +
126, 10, 11co 6296 . . . . . . . . 9  class  ( i  +  1 )
1312, 8cfv 5592 . . . . . . . 8  class  ( w `
 ( i  +  1 ) )
149, 13cpr 3995 . . . . . . 7  class  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }
153cv 1436 . . . . . . . 8  class  e
1615crn 4846 . . . . . . 7  class  ran  e
1714, 16wcel 1867 . . . . . 6  wff  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
18 cc0 9528 . . . . . . 7  class  0
19 chash 12501 . . . . . . . . 9  class  #
208, 19cfv 5592 . . . . . . . 8  class  ( # `  w )
21 cmin 9849 . . . . . . . 8  class  -
2220, 10, 21co 6296 . . . . . . 7  class  ( (
# `  w )  -  1 )
23 cfzo 11902 . . . . . . 7  class ..^
2418, 22, 23co 6296 . . . . . 6  class  ( 0..^ ( ( # `  w
)  -  1 ) )
2517, 5, 24wral 2773 . . . . 5  wff  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
26 clsw 12633 . . . . . . . 8  class lastS
278, 26cfv 5592 . . . . . . 7  class  ( lastS  `  w
)
2818, 8cfv 5592 . . . . . . 7  class  ( w `
 0 )
2927, 28cpr 3995 . . . . . 6  class  { ( lastS  `  w ) ,  ( w `  0 ) }
3029, 16wcel 1867 . . . . 5  wff  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  e
3125, 30wa 370 . . . 4  wff  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e )
322cv 1436 . . . . 5  class  v
3332cword 12632 . . . 4  class Word  v
3431, 7, 33crab 2777 . . 3  class  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) }
352, 3, 4, 4, 34cmpt2 6298 . 2  class  ( v  e.  _V ,  e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
361, 35wceq 1437 1  wff ClWWalks  =  ( v  e.  _V , 
e  e.  _V  |->  { w  e. Word  v  |  ( A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e ) } )
Colors of variables: wff setvar class
This definition is referenced by:  clwwlk  25336  clwwlkprop  25340
  Copyright terms: Public domain W3C validator