Definition df-clwwlknon

Description: Define the set of all closed walks a graph g , anchored at a fixed vertex v (i.e., a walk starting and ending at the fixed vertex v , also called "a closed walk on vertex v ") and having a fixed length n as words over the set of vertices. Such a word corresponds to the sequence v=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)=v as defined in df-clwlks . The set ( ( v ( ClWWalksNOng ) n ) corresponds to the set of "walks from v to v of length n" in a statement of Huneke p. 2. (Contributed by AV, 24-Feb-2022)

	Ref	Expression
Assertion	df-clwwlknon	|- ClWWalksNOn = ( g e. _V |-> ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cclwwlknon	|- ClWWalksNOn
1		vg	|- g
2		cvv	|- _V
3		vv	|- v
4		cvtx	|- Vtx
5	1	cv	|- g
6	5 4	cfv	|- ( Vtx ` g )
7		vn	|- n
8		cn0	|- NN0
9		vw	|- w
10	7	cv	|- n
11		cclwwlkn	|- ClWWalksN
12	10 5 11	co	|- ( n ClWWalksN g )
13	9	cv	|- w
14		cc0	|- 0
15	14 13	cfv	|- ( w ` 0 )
16	3	cv	|- v
17	15 16	wceq	|- ( w ` 0 ) = v
18	17 9 12	crab	|- { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v }
19	3 7 6 8 18	cmpo	|- ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } )
20	1 2 19	cmpt	|- ( g e. _V |-> ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
21	0 20	wceq	|- ClWWalksNOn = ( g e. _V |-> ( v e. ( Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )