Theorem hashclwwlkn0

Description: 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) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Hypotheses	erclwwlkn.w	|- W = ( N ClWWalksN G )
	erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
Assertion	hashclwwlkn0	|- ( ( Vtx ` G ) e. Fin -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	|- W = ( N ClWWalksN G )
2		erclwwlkn.r	|- .~ = { <. t , u >. | ( t e. W /\ u e. W /\ E. n e. ( 0 ... N ) t = ( u cyclShift n ) ) }
3	1 2	erclwwlkn	|- .~ Er W
4	3	a1i	|- ( ( Vtx ` G ) e. Fin -> .~ Er W )
5		clwwlknfi	|- ( ( Vtx ` G ) e. Fin -> ( N ClWWalksN G ) e. Fin )
6	1 5	eqeltrid	|- ( ( Vtx ` G ) e. Fin -> W e. Fin )
7	4 6	qshash	|- ( ( Vtx ` G ) e. Fin -> ( # ` W ) = sum_ x e. ( W /. .~ ) ( # ` x ) )