Metamath Proof Explorer

Theorem clwwlknwrd

Description: A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021)

Ref Expression
Hypothesis clwwlknwrd.v ⊢ V = Vtx ⁡ G
Assertion clwwlknwrd ⊢ W ∈ N ClWWalksN G → W ∈ Word V

Proof

Step Hyp Ref Expression
1 clwwlknwrd.v ⊢ V = Vtx ⁡ G
2 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
3 1 clwwlkbp ⊢ W ∈ ClWWalks ⁡ G → G ∈ V ∧ W ∈ Word V ∧ W ≠ ∅
4 3 simp2d ⊢ W ∈ ClWWalks ⁡ G → W ∈ Word V
5 4 adantr ⊢ W ∈ ClWWalks ⁡ G ∧ W = N → W ∈ Word V
6 2 5 sylbi ⊢ W ∈ N ClWWalksN G → W ∈ Word V