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	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		isclwwlkn	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
2	1	simprbi	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )