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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	clwwlknwrd	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ Word 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		clwwlknwrd.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isclwwlkn	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ↔ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) )
3	1	clwwlkbp	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ) )
4	3	simp2d	⊢ ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 )
5	4	adantr	⊢ ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ) → 𝑊 ∈ Word 𝑉 )
6	2 5	sylbi	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ Word 𝑉 )