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

Metamath Proof Explorer

Theorem clwwlknbp

Description: Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Hypothesis clwwlknwrd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion clwwlknbp ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 clwwlknwrd.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 clwwlknwrd ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ Word 𝑉 )
3 clwwlknlen ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( ♯ ‘ 𝑊 ) = 𝑁 )
4 2 3 jca ⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )