This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwlknlen

Description: The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022)

		Ref	Expression
	Assertion	clwwlknlen	$⊢ W \in (N ClWWalksN G) \to \|W\| = N$

Step	Hyp	Ref	Expression
1		isclwwlkn	$⊢ W \in (N ClWWalksN G) \leftrightarrow (W \in ClWWalks (G) \land \|W\| = N)$
2	1	simprbi	$⊢ W \in (N ClWWalksN G) \to \|W\| = N$