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	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	clwwlknbp	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \left(W\in \mathrm{Word}V\wedge \left|W\right|=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		clwwlknwrd.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	clwwlknwrd	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to W\in \mathrm{Word}V$$
3		clwwlknlen	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \left|W\right|=N$$
4	2 3	jca	$$⊢W\in \left(N\mathrm{ClWWalksN}G\right)\to \left(W\in \mathrm{Word}V\wedge \left|W\right|=N\right)$$