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

Definition df-clwwlk 24415
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 24414. 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 24454. (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 24412 . 2  class ClWWalks
2 vv . . 3  setvar  v
3 ve . . 3  setvar  e
4 cvv 3108 . . 3  class  _V
5 vi . . . . . . . . . 10  setvar  i
65cv 1373 . . . . . . . . 9  class  i
7 vw . . . . . . . . . 10  setvar  w
87cv 1373 . . . . . . . . 9  class  w
96, 8cfv 5581 . . . . . . . 8  class  ( w `
 i )
10 c1 9484 . . . . . . . . . 10  class  1
11 caddc 9486 . . . . . . . . . 10  class  +
126, 10, 11co 6277 . . . . . . . . 9  class  ( i  +  1 )
1312, 8cfv 5581 . . . . . . . 8  class  ( w `
 ( i  +  1 ) )
149, 13cpr 4024 . . . . . . 7  class  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }
153cv 1373 . . . . . . . 8  class  e
1615crn 4995 . . . . . . 7  class  ran  e
1714, 16wcel 1762 . . . . . 6  wff  { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
18 cc0 9483 . . . . . . 7  class  0
19 chash 12362 . . . . . . . . 9  class  #
208, 19cfv 5581 . . . . . . . 8  class  ( # `  w )
21 cmin 9796 . . . . . . . 8  class  -
2220, 10, 21co 6277 . . . . . . 7  class  ( (
# `  w )  -  1 )
23 cfzo 11783 . . . . . . 7  class ..^
2418, 22, 23co 6277 . . . . . 6  class  ( 0..^ ( ( # `  w
)  -  1 ) )
2517, 5, 24wral 2809 . . . . 5  wff  A. i  e.  ( 0..^ ( (
# `  w )  -  1 ) ) { ( w `  i ) ,  ( w `  ( i  +  1 ) ) }  e.  ran  e
26 clsw 12490 . . . . . . . 8  class lastS
278, 26cfv 5581 . . . . . . 7  class  ( lastS  `  w
)
2818, 8cfv 5581 . . . . . . 7  class  ( w `
 0 )
2927, 28cpr 4024 . . . . . 6  class  { ( lastS  `  w ) ,  ( w `  0 ) }
3029, 16wcel 1762 . . . . 5  wff  { ( lastS  `  w ) ,  ( w `  0 ) }  e.  ran  e
3125, 30wa 369 . . . 4  wff  ( A. i  e.  ( 0..^ ( ( # `  w
)  -  1 ) ) { ( w `
 i ) ,  ( w `  (
i  +  1 ) ) }  e.  ran  e  /\  { ( lastS  `  w
) ,  ( w `
 0 ) }  e.  ran  e )
322cv 1373 . . . . 5  class  v
3332cword 12489 . . . 4  class Word  v
3431, 7, 33crab 2813 . . 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 6279 . 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 1374 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  24430  clwwlkprop  24434
  Copyright terms: Public domain W3C validator