Definition df-clwwlk 16130

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 elsewhere. 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. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)

Assertion

Ref	Expression
df-clwwlk	|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )

Distinct variable group:   g, i, w

Detailed syntax breakdown of Definition df-clwwlk

Step	Hyp	Ref	Expression
1		cclwwlk 16129	. 2 class ClWWalks
2		vg	. . 3 setvar g
3		cvv 2799	. . 3 class _V
4		vw	. . . . . . 7 setvar w
5	4	cv 1394	. . . . . 6 class w
6		c0 3491	. . . . . 6 class (/)
7	5, 6	wne 2400	. . . . 5 wff w =/= (/)
8		vi	. . . . . . . . . 10 setvar i
9	8	cv 1394	. . . . . . . . 9 class i
10	9, 5	cfv 5318	. . . . . . . 8 class ( w ` i )
11		c1 8011	. . . . . . . . . 10 class 1
12		caddc 8013	. . . . . . . . . 10 class +
13	9, 11, 12	co 6007	. . . . . . . . 9 class ( i + 1 )
14	13, 5	cfv 5318	. . . . . . . 8 class ( w ` ( i + 1 ) )
15	10, 14	cpr 3667	. . . . . . 7 class { ( w ` i ) , ( w ` ( i + 1 ) ) }
16	2	cv 1394	. . . . . . . 8 class g
17		cedg 15873	. . . . . . . 8 class Edg
18	16, 17	cfv 5318	. . . . . . 7 class (Edg ` g )
19	15, 18	wcel 2200	. . . . . 6 wff { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
20		cc0 8010	. . . . . . 7 class 0
21		chash 11009	. . . . . . . . 9 class ♯
22	5, 21	cfv 5318	. . . . . . . 8 class (♯ ` w )
23		cmin 8328	. . . . . . . 8 class -
24	22, 11, 23	co 6007	. . . . . . 7 class ( (♯ ` w ) - 1 )
25		cfzo 10350	. . . . . . 7 class ..^
26	20, 24, 25	co 6007	. . . . . 6 class ( 0..^ ( (♯ ` w ) - 1 ) )
27	19, 8, 26	wral 2508	. . . . 5 wff A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g )
28		clsw 11129	. . . . . . . 8 class lastS
29	5, 28	cfv 5318	. . . . . . 7 class (lastS ` w )
30	20, 5	cfv 5318	. . . . . . 7 class ( w ` 0 )
31	29, 30	cpr 3667	. . . . . 6 class { (lastS ` w ) , ( w ` 0 ) }
32	31, 18	wcel 2200	. . . . 5 wff { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g )
33	7, 27, 32	w3a 1002	. . . 4 wff ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) )
34		cvtx 15828	. . . . . 6 class Vtx
35	16, 34	cfv 5318	. . . . 5 class (Vtx ` g )
36	35	cword 11084	. . . 4 class Word (Vtx ` g )
37	33, 4, 36	crab 2512	. . 3 class { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) }
38	2, 3, 37	cmpt 4145	. 2 class ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
39	1, 38	wceq 1395	1 wff ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )

This definition is referenced by:  clwwlkg  16131  isclwwlk  16132  clwwlkbp  16133