P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	disjxwwlks 25401*	Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 29-Jul-2018.)
|- Disj y e. ( ( V WWalksN E ) ` N ) { x e. Word V | ( ( x substr <. 0 , N >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. ran E ) }
Theorem	wwlknndef 25402	Conditions for WWalksN not being defined. (Contributed by Alexander van der Vekens, 30-Jul-2018.)
|- ( ( V e/ _V \/ E e/ _V \/ N e/ NN0 ) -> ( ( V WWalksN E ) ` N ) = (/) )
Theorem	wwlknfi 25403	The number of walks represented by words of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 30-Jul-2018.)
|- ( V e. Fin -> ( ( V WWalksN E ) ` N ) e. Fin )
Theorem	wlknfi 25404*	The number of walks of fixed length is finite if the number of vertices is finite (in the graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( ( V USGrph E /\ N e. NN0 /\ V e. Fin ) -> { p e. ( V Walks E ) | ( # ` ( 1st ` p ) ) = N } e. Fin )
Theorem	wlknwwlknvbij 25405*	There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length and starting at the same vertex. (Contributed by Alexander van der Vekens, 30-Sep-2018.)
|- ( ( V USGrph E /\ N e. NN0 /\ X e. V ) -> E. f f : { p e. ( V Walks E ) | ( ( # ` ( 1st ` p ) ) = N /\ ( ( 2nd ` p ) ` 0 ) = X ) } -1-1-onto-> { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = X } )
Theorem	wwlkextproplem1 25406	Lemma 1 for wwlkextprop 25409. (Contributed by Alexander van der Vekens, 31-Jul-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   =>    |- ( ( W e. X /\ N e. NN0 ) -> ( ( W substr <. 0 , ( N + 1 ) >. ) ` 0 ) = ( W ` 0 ) )
Theorem	wwlkextproplem2 25407	Lemma 2 for wwlkextprop 25409. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   =>    |- ( ( W e. X /\ N e. NN0 ) -> { ( lastS ` ( W substr <. 0 , ( N + 1 ) >. ) ) , ( lastS ` W ) } e. ran E )
Theorem	wwlkextproplem3 25408*	Lemma 3 for wwlkextprop 25409. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   &    |- Y = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   =>    |- ( ( W e. X /\ ( W ` 0 ) = P /\ N e. NN0 ) -> ( W substr <. 0 , ( N + 1 ) >. ) e. Y )
Theorem	wwlkextprop 25409*	Adding additional properties to the set of walks (as words) of a fixed length starting at a fixed vertex. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   &    |- Y = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   =>    |- ( N e. NN0 -> { x e. X | ( x ` 0 ) = P } = { x e. X | E. y e. Y ( ( x substr <. 0 , ( N + 1 ) >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. ran E ) } )
Theorem	disjxwwlkn 25410*	Sets of walks (as words) extended by an edge are disjunct if each set contains extensions of distinct walks. (Contributed by Alexander van der Vekens, 21-Aug-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   &    |- Y = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   =>    |- Disj y e. Y { x e. X | ( ( x substr <. 0 , M >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. ran E ) }
Theorem	hashwwlkext 25411*	Number of walks (as words) extended by an edge as sum over the prefixes. (Contributed by Alexander van der Vekens, 21-Aug-2018.)
|- X = ( ( V WWalksN E ) ` ( N + 1 ) )   &    |- Y = { w e. ( ( V WWalksN E ) ` N ) | ( w ` 0 ) = P }   =>    |- ( V e. Fin -> ( # ` { x e. X | E. y e. Y ( ( x substr <. 0 , M >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. ran E ) } ) = sum_ y e. Y ( # ` { x e. X | ( ( x substr <. 0 , M >. ) = y /\ ( y ` 0 ) = P /\ { ( lastS ` y ) , ( lastS ` x ) } e. ran E ) } ) )
16.1.5.6  Closed walks
Syntax	cclwlk 25412	Extend class notation with Closed Walks (of a graph).
class ClWalks
Syntax	cclwwlk 25413	Extend class notation with Closed Walks (of a graph) as Word over the set of vertices.
class ClWWalks
Syntax	cclwwlkn 25414	Extend class notation with Closed Walks (of a graph) of a fixed length as Word over the set of vertices.
class ClWWalksN
Definition	df-clwlk 25415*	Define the set of all Closed Walks (in an undirected graph). According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). Notice that by this definition, a single vertex is a closed walk of length 0, see also 0clwlk 25430! (Contributed by Alexander van der Vekens, 12-Mar-2018.)
|- ClWalks = ( v e. _V , e e. _V |-> { <. f , p >. | ( f ( v Walks e ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
Definition	df-clwwlk 25416*	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 25415. 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 25455. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- 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 ) } )
Definition	df-clwwlkn 25417*	Define the set of all Closed Walks (in an undirected graph) of a fixed length n 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 25415. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- ClWWalksN = ( v e. _V , e e. _V |-> ( n e. NN0 |-> { w e. ( v ClWWalks e ) | ( # ` w ) = n } ) )
Theorem	clwlk 25418*	The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V ClWalks E ) = { <. f , p >. | ( f ( V Walks E ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
Theorem	isclwlk0 25419	Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( V ClWalks E ) P <-> ( F ( V Walks E ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	isclwlkg 25420	Generalisation of isclwlk0 25419: Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( F ( V ClWalks E ) P <-> ( F ( V Walks E ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	isclwlk 25421*	Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( F ( V ClWalks E ) P <-> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
Theorem	clwlkiswlk 25422	A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( F ( V ClWalks E ) P -> F ( V Walks E ) P )
Theorem	clwlkswlks 25423	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.)
|- ( W e. ( V ClWalks E ) -> W e. ( V Walks E ) )
Theorem	clwlksarewlks 25424	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.)
|- ( V ClWalks E ) C_ ( V Walks E )
Theorem	wlkv0 25425	If there is a walk in an empty graph, it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
|- ( W e. ( (/) Walks E ) -> ( ( 1st ` W ) = (/) /\ ( 2nd ` W ) = (/) ) )
Theorem	wlk0 25426	There is no walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
|- ( (/) Walks E ) = (/)
Theorem	clwlk0 25427	There is no closed walk in an empty graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.)
|- ( (/) ClWalks E ) = (/)
Theorem	clwlkcomp 25428*	A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
|- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( ( V e. X /\ E e. Y /\ W e. ( S X. T ) ) -> ( W e. ( V ClWalks E ) <-> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )
Theorem	clwlkcompim 25429*	Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.)
|- F = ( 1st ` W )   &    |- P = ( 2nd ` W )   =>    |- ( W e. ( V ClWalks E ) -> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0..^ ( # ` F ) ) ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	0clwlk 25430	A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ P e. Z ) -> ( (/) ( V ClWalks E ) P <-> P : ( 0 ... 0 ) --> V ) )
Theorem	clwwlk 25431*	The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V ClWWalks E ) = { 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 ) } )
Theorem	clwwlkn 25432*	The set of closed walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( ( V ClWWalksN E ) ` N ) = { w e. ( V ClWWalks E ) | ( # ` w ) = N } )
Theorem	isclwwlk 25433*	Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( W e. ( V ClWWalks E ) <-> ( 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 ) ) )
Theorem	isclwwlkn 25434	Properties of a word to represent a closed walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( W e. ( ( V ClWWalksN E ) ` N ) <-> ( W e. ( V ClWWalks E ) /\ ( # ` W ) = N ) ) )
Theorem	clwwlkprop 25435	Properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( P e. ( V ClWWalks E ) -> ( V e. _V /\ E e. _V /\ P e. Word V ) )
Theorem	clwwlkgt0 25436	A closed walk in an undirected graph has a length of at least 2. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
|- ( V USGrph E -> ( P e. ( V ClWWalks E ) -> 2 <_ ( # ` P ) ) )
Theorem	clwwlknprop 25437	Properties of a closed walk of a fixed length as word. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- ( P e. ( ( V ClWWalksN E ) ` N ) -> ( ( V e. _V /\ E e. _V ) /\ P e. Word V /\ ( N e. NN0 /\ ( # ` P ) = N ) ) )
Theorem	clwwlknndef 25438	Conditions for ClWWalksN not being defined. (Contributed by Alexander van der Vekens, 15-Sep-2018.)
|- ( ( V e/ _V \/ E e/ _V \/ N e/ NN0 ) -> ( ( V ClWWalksN E ) ` N ) = (/) )
Theorem	clwwlkn0 25439	There is no closed walk of length 0 in an undirected simple graph. (Contributed by Alexander van der Vekens, 15-Sep-2018.)
|- ( V USGrph E -> ( ( V ClWWalksN E ) ` 0 ) = (/) )
Theorem	clwwlkn2 25440	In an undirected simple graph, a closed walk of length 2 represented as word is a word consisting of 2 symbols representing vertices connected by an edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.)
|- ( V USGrph E -> ( W e. ( ( V ClWWalksN E ) ` 2 ) <-> ( ( # ` W ) = 2 /\ W e. Word V /\ { ( W ` 0 ) , ( W ` 1 ) } e. ran E ) ) )
Theorem	clwwlknimp 25441*	Implications for a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( W e. ( ( V ClWWalksN E ) ` N ) -> ( ( W e. Word V /\ ( # ` W ) = N ) /\ A. i e. ( 0..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` W ) , ( W ` 0 ) } e. ran E ) )
Theorem	clwwlksswrd 25442	Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V ClWWalks E ) C_ Word V )
Theorem	clwwlknfi 25443	If there is only a finite number of vertices, the number of closed walk of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- ( ( V e. Fin /\ E e. X /\ N e. NN0 ) -> ( ( V ClWWalksN E ) ` N ) e. Fin )
Theorem	clwlkisclwwlklem2a1 25444*	Lemma 1 for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 21-Jun-2018.)
|- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> A. i e. ( 0..^ ( ( # ` P ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E ) )
Theorem	clwlkisclwwlklem2a2 25445*	Lemma 3 for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 21-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( # ` F ) = ( ( # ` P ) - 1 ) )
Theorem	clwlkisclwwlklem2a3 25446*	Lemma 3 for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 21-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( P e. Word V /\ 2 <_ ( # ` P ) ) -> ( P ` ( # ` F ) ) = ( lastS ` P ) )
Theorem	clwlkisclwwlklem2fv1 25447*	Lemma 4a for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( ( # ` P ) e. NN0 /\ I e. ( 0..^ ( ( # ` P ) - 2 ) ) ) -> ( F ` I ) = ( `' E ` { ( P ` I ) , ( P ` ( I + 1 ) ) } ) )
Theorem	clwlkisclwwlklem2fv2 25448*	Lemma 4b for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( ( # ` P ) e. NN0 /\ 2 <_ ( # ` P ) ) -> ( F ` ( ( # ` P ) - 2 ) ) = ( `' E ` { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } ) )
Theorem	clwlkisclwwlklem2a4 25449*	Lemma 4 for clwlkisclwwlklem2a 25450. (Contributed by Alexander van der Vekens, 21-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ I e. ( 0..^ ( ( # ` P ) - 1 ) ) ) -> ( { ( P ` I ) , ( P ` ( I + 1 ) ) } e. ran E -> ( E ` ( F ` I ) ) = { ( P ` I ) , ( P ` ( I + 1 ) ) } ) ) )
Theorem	clwlkisclwwlklem2a 25450*	Lemma 2 for clwlkisclwwlklem2 25451. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- F = ( x e. ( 0..^ ( ( # ` P ) - 1 ) ) |-> if ( x < ( ( # ` P ) - 2 ) , ( `' E ` { ( P ` x ) , ( P ` ( x + 1 ) ) } ) , ( `' E ` { ( P ` x ) , ( P ` 0 ) } ) ) )   =>    |- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> ( ( F e. Word dom E /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	clwlkisclwwlklem2 25451*	Lemma for clwlkisclwwlk 25454. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) -> E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) ) )
Theorem	clwlkisclwwlklem1 25452*	Lemma for clwlkisclwwlk 25454. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- ( ( ( V USGrph E /\ F e. Word dom E ) /\ ( P : ( 0 ... ( # ` F ) ) --> V /\ 2 <_ ( # ` P ) ) /\ ( A. i e. ( 0..^ ( # ` F ) ) ( E ` ( F ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) -> ( ( lastS ` P ) = ( P ` 0 ) /\ A. i e. ( 0..^ ( ( # ` F ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` F ) - 1 ) ) , ( P ` 0 ) } e. ran E ) )
Theorem	clwlkisclwwlklem0 25453*	Lemma for clwlkisclwwlk 25454. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f ( ( f e. Word dom E /\ P : ( 0 ... ( # ` f ) ) --> V /\ A. i e. ( 0..^ ( # ` f ) ) ( E ` ( f ` i ) ) = { ( P ` i ) , ( P ` ( i + 1 ) ) } ) /\ ( P ` 0 ) = ( P ` ( # ` f ) ) ) <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( A. i e. ( 0..^ ( ( ( ( # ` P ) - 1 ) - 0 ) - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( P ` ( ( # ` P ) - 2 ) ) , ( P ` 0 ) } e. ran E ) ) ) )
Theorem	clwlkisclwwlk 25454*	A closed walk as word corresponds to a closed walk in an undirected graph. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- ( ( V USGrph E /\ P e. Word V /\ 2 <_ ( # ` P ) ) -> ( E. f f ( V ClWalks E ) P <-> ( ( lastS ` P ) = ( P ` 0 ) /\ ( P substr <. 0 , ( ( # ` P ) - 1 ) >. ) e. ( V ClWWalks E ) ) ) )
Theorem	clwlkisclwwlk2 25455*	A closed walk corresponds to a closed walk as word in an undirected graph. (Contributed by Alexander van der Vekens, 22-Jun-2018.)
|- ( ( V USGrph E /\ P e. Word V /\ 1 <_ ( # ` P ) ) -> ( E. f f ( V ClWalks E ) ( P ++ <" ( P ` 0 ) "> ) <-> P e. ( V ClWWalks E ) ) )
Theorem	clwwlkisclwwlkn 25456	A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( P e. ( ( V ClWWalksN E ) ` N ) -> P e. ( V ClWWalks E ) ) )
Theorem	clwwlkssclwwlkn 25457	The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN0 ) -> ( ( V ClWWalksN E ) ` N ) C_ ( V ClWWalks E ) )
Theorem	clwwlkel 25458*	Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 20-Oct-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   =>    |- ( ( ( V e. X /\ E e. Y /\ N e. NN ) /\ ( P e. Word V /\ ( # ` P ) = N ) /\ ( A. i e. ( 0..^ ( N - 1 ) ) { ( P ` i ) , ( P ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` P ) , ( P ` 0 ) } e. ran E ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. D )
Theorem	clwwlkf 25459*	Lemma 1 for clwwlkbij 25464: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   &    |- F = ( t e. D |-> ( t substr <. 0 , N >. ) )   =>    |- ( ( V e. X /\ E e. Y /\ N e. NN ) -> F : D --> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwwlkfv 25460*	Lemma 2 for clwwlkbij 25464: the value of function F. (Contributed by Alexander van der Vekens, 28-Sep-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   &    |- F = ( t e. D |-> ( t substr <. 0 , N >. ) )   =>    |- ( W e. D -> ( F ` W ) = ( W substr <. 0 , N >. ) )
Theorem	clwwlkf1 25461*	Lemma 3 for clwwlkbij 25464: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   &    |- F = ( t e. D |-> ( t substr <. 0 , N >. ) )   =>    |- ( ( V e. X /\ E e. Y /\ N e. NN ) -> F : D -1-1-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwwlkfo 25462*	Lemma 4 for clwwlkbij 25464: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   &    |- F = ( t e. D |-> ( t substr <. 0 , N >. ) )   =>    |- ( ( V e. X /\ E e. Y /\ N e. NN ) -> F : D -onto-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwwlkf1o 25463*	Lemma 5 for clwwlkbij 25464: F is a 1-1 onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- D = { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) }   &    |- F = ( t e. D |-> ( t substr <. 0 , N >. ) )   =>    |- ( ( V e. X /\ E e. Y /\ N e. NN ) -> F : D -1-1-onto-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwwlkbij 25464*	There is a bijection between the set of closed walks of a fixed length represented by walks (as word) and the set of closed walks (as words) of a fixed length. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN ) -> E. f f : { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) } -1-1-onto-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwwlknwwlkncl 25465*	Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- ( ( N e. NN /\ P e. ( ( V ClWWalksN E ) ` N ) ) -> ( P ++ <" ( P ` 0 ) "> ) e. { w e. ( ( V WWalksN E ) ` N ) | ( lastS ` w ) = ( w ` 0 ) } )
Theorem	clwwlkvbij 25466*	There is a bijection between the set of closed walks of a fixed length starting at a fixed vertex represented by walks (as word) and the set of closed walks (as words) of a fixed length starting at a fixed vertex. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.)
|- ( ( V e. X /\ E e. Y /\ N e. NN ) -> E. f f : { w e. ( ( V WWalksN E ) ` N ) | ( ( lastS ` w ) = ( w ` 0 ) /\ ( w ` 0 ) = S ) } -1-1-onto-> { w e. ( ( V ClWWalksN E ) ` N ) | ( w ` 0 ) = S } )
Theorem	clwwlkext2edg 25467	If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" Z "> ) e. ( ( V ClWWalksN E ) ` N ) ) -> ( { ( lastS ` W ) , Z } e. ran E /\ { Z , ( W ` 0 ) } e. ran E ) )
Theorem	wwlkext2clwwlk 25468	If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
|- ( ( W e. ( ( V WWalksN E ) ` N ) /\ Z e. V /\ N e. NN0 ) -> ( ( { ( lastS ` W ) , Z } e. ran E /\ { Z , ( W ` 0 ) } e. ran E ) -> ( W ++ <" Z "> ) e. ( ( V ClWWalksN E ) ` ( N + 2 ) ) ) )
Theorem	wwlksubclwwlk 25469	Any prefix of a word representing a closed walk represents a word. (Contributed by Alexander van der Vekens, 5-Oct-2018.)
|- ( ( M e. NN /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( X e. ( ( V ClWWalksN E ) ` N ) -> ( X substr <. 0 , M >. ) e. ( ( V WWalksN E ) ` ( M - 1 ) ) ) )
Theorem	clwwisshclwwlem1 25470*	Lemma 1 for clwwisshclwwlem 25471. (Contributed by Alexander van der Vekens, 23-Mar-2018.)
|- ( ( ( L e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ B e. ZZ ) /\ A. i e. ( 0..^ ( L - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. R /\ { ( W ` ( L - 1 ) ) , ( W ` 0 ) } e. R ) -> { ( W ` ( ( A + B ) mod L ) ) , ( W ` ( ( ( A + 1 ) + B ) mod L ) ) } e. R )
Theorem	clwwisshclwwlem 25471*	Lemma for clwwisshclww 25472. (Contributed by AV, 24-Mar-2018.) (Revised by AV, 10-Jun-2018.) (Proof shortened by AV, 2-Nov-2018.)
|- ( ( W e. Word V /\ N e. ( 1..^ ( # ` W ) ) ) -> ( ( A. i e. ( 0..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ran E /\ { ( lastS ` W ) , ( W ` 0 ) } e. ran E ) -> A. j e. ( 0..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ran E ) )
Theorem	clwwisshclww 25472	Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Mar-2018.) (Revised by Alexander van der Vekens, 10-Jun-2018.)
|- ( ( W e. ( V ClWWalks E ) /\ N e. ( 0..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. ( V ClWWalks E ) )
Theorem	clwwisshclwwn 25473	Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|- ( ( W e. ( V ClWWalks E ) /\ N e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift N ) e. ( V ClWWalks E ) )
Theorem	clwwnisshclwwn 25474	Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018.)
|- ( ( N e. NN0 /\ W e. ( ( V ClWWalksN E ) ` N ) ) -> ( M e. ( 0 ... N ) -> ( W cyclShift M ) e. ( ( V ClWWalksN E ) ` N ) ) )
Theorem	erclwwlkrel 25475	.~ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- Rel .~
Theorem	erclwwlkeq 25476*	Two classes are equivalent regarding .~ if both are words and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- ( ( U e. X /\ W e. Y ) -> ( U .~ W <-> ( U e. ( V ClWWalks E ) /\ W e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` W ) ) U = ( W cyclShift n ) ) ) )
Theorem	erclwwlkeqlen 25477*	If two classes are equivalent regarding .~, then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- ( ( U e. X /\ W e. Y ) -> ( U .~ W -> ( # ` U ) = ( # ` W ) ) )
Theorem	erclwwlkref 25478*	.~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- ( x e. ( V ClWWalks E ) <-> x .~ x )
Theorem	erclwwlksym 25479*	.~ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- ( x .~ y -> y .~ x )
Theorem	erclwwlktr 25480*	.~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- ( ( x .~ y /\ y .~ z ) -> x .~ z )
Theorem	erclwwlk 25481*	.~ is an equivalence relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.)
|- .~ = { <. u , w >. | ( u e. ( V ClWWalks E ) /\ w e. ( V ClWWalks E ) /\ E. n e. ( 0 ... ( # ` w ) ) u = ( w cyclShift n ) ) }   =>    |- .~ Er ( V ClWWalks E )
Theorem	eleclclwwlknlem1 25482*	Lemma 1 for eleclclwwlkn 25498. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   =>    |- ( ( K e. ( 0 ... N ) /\ ( X e. W /\ Y e. W ) ) -> ( ( X = ( Y cyclShift K ) /\ E. m e. ( 0 ... N ) Z = ( Y cyclShift m ) ) -> E. n e. ( 0 ... N ) Z = ( X cyclShift n ) ) )
Theorem	eleclclwwlknlem2 25483*	Lemma 2 for eleclclwwlkn 25498. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   =>    |- ( ( ( k e. ( 0 ... N ) /\ X = ( x cyclShift k ) ) /\ ( X e. W /\ x e. W ) ) -> ( E. m e. ( 0 ... N ) Y = ( x cyclShift m ) <-> E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) )
Theorem	clwwlknscsh 25484*	The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
|- ( ( N e. NN0 /\ W e. ( ( V ClWWalksN E ) ` N ) ) -> { y e. ( ( V ClWWalksN E ) ` N ) | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } = { y e. Word V | E. n e. ( 0 ... N ) y = ( W cyclShift n ) } )
Theorem	usg2cwwk2dif 25485	If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( ( V USGrph E /\ N e. ( ZZ>= ` 2 ) /\ W e. ( ( V ClWWalksN E ) ` N ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )
Theorem	usg2cwwkdifex 25486*	If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( ( V USGrph E /\ N e. ( ZZ>= ` 2 ) /\ W e. ( ( V ClWWalksN E ) ` N ) ) -> E. i e. ( 0..^ N ) ( W ` i ) =/= ( W ` 0 ) )
Theorem	erclwwlknrel 25487	.~ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- Rel .~
Theorem	erclwwlkneq 25488*	Two classes are equivalent regarding .~ if both are words of the same fixed length and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( T e. X /\ U e. Y ) -> ( T .~ U <-> ( T e. W /\ U e. W /\ E. n e. ( 0 ... N ) T = ( U cyclShift n ) ) ) )
Theorem	erclwwlkneqlen 25489*	If two classes are equivalent regarding .~, then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( T e. X /\ U e. Y ) -> ( T .~ U -> ( # ` T ) = ( # ` U ) ) )
Theorem	erclwwlknref 25490*	.~ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( x e. W <-> x .~ x )
Theorem	erclwwlknsym 25491*	.~ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( x .~ y -> y .~ x )
Theorem	erclwwlkntr 25492*	.~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( x .~ y /\ y .~ z ) -> x .~ z )
Theorem	erclwwlkn 25493*	.~ is an equivalence relation over the set of closed walks (defined as words) with a fixed length. (Contributed by Alexander van der Vekens, 10-Apr-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- .~ Er W
Theorem	qerclwwlknfi 25494*	The quotient set of the set of closed walks (defined as words) with a fixed length according to the equivalence relation .~ is finite. (Contributed by Alexander van der Vekens, 10-Apr-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( V e. Fin /\ E e. X /\ N e. NN0 ) -> ( W /. .~ ) e. Fin )
Theorem	hashclwwlkn0 25495*	The number of closed walks (defined as words) with a fixed length is the sum of the sizes of all equivalence classes according to .~. (Contributed by Alexander van der Vekens, 10-Apr-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( V e. Fin /\ E e. X /\ N e. NN0 ) -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )
Theorem	eclclwwlkn0 25496*	An equivalence class according to .~. (Contributed by Alexander van der Vekens, 12-Apr-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y | x .~ y } ) )
Theorem	eclclwwlkn1 25497*	An equivalence class according to .~. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by Alexander van der Vekens, 15-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( B e. X -> ( B e. ( W /. .~ ) <-> E. x e. W B = { y e. W | E. n e. ( 0 ... N ) y = ( x cyclShift n ) } ) )
Theorem	eleclclwwlkn 25498*	A member of an equivalence class according to .~. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 15-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( B e. ( W /. .~ ) /\ X e. B ) -> ( Y e. B <-> ( Y e. W /\ E. n e. ( 0 ... N ) Y = ( X cyclShift n ) ) ) )
Theorem	hashecclwwlkn1 25499*	The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( N e. Prime /\ U e. ( W /. .~ ) ) -> ( ( # ` U ) = 1 \/ ( # ` U ) = N ) )
Theorem	usghashecclwwlk 25500*	The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number equals this length (in an undirected simple graph). (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- W = ( ( V ClWWalksN E ) ` N )   &    |- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }   =>    |- ( ( V USGrph E /\ N e. Prime ) -> ( U e. ( W /. .~ ) -> ( # ` U ) = N ) )