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

Proof

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