Theorem clwwnrepclwwn

Description: If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk. Notice that 3 <_ N is required, because for N = 2 , ( w prefix ( N - 2 ) ) = ( w prefix 0 ) = (/) , but (/) (and anything else) is not a representation of an empty closed walk as word, see clwwlkn0 . (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 28-May-2021) (Revised by AV, 30-Oct-2022)

	Ref	Expression
Assertion	clwwnrepclwwn	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		uz3m2nn	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 2 ) ∈ ℕ )
2		eluzelz	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝑁 ∈ ℤ )
3		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
4		subeluzsub	⊢ ( ( 𝑁 ∈ ℤ ∧ 2 ∈ ( ℤ≥ ‘ 1 ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 2 ) ) )
5	2 3 4	sylancl	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 2 ) ) )
6	1 5	jca	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( ( 𝑁 − 2 ) ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 2 ) ) ) )
7	6	3ad2ant1	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( ( 𝑁 − 2 ) ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 2 ) ) ) )
8		clwwlknwwlksn	⊢ ( 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) → 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) )
9	8	3ad2ant2	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) )
10		simp3	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) )
11		clwwlkinwwlk	⊢ ( ( ( ( 𝑁 − 2 ) ∈ ℕ ∧ ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 2 ) ) ) ∧ 𝑊 ∈ ( ( 𝑁 − 1 ) WWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) )
12	7 9 10 11	syl3anc	⊢ ( ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) ∧ 𝑊 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( 𝑊 ‘ ( 𝑁 − 2 ) ) = ( 𝑊 ‘ 0 ) ) → ( 𝑊 prefix ( 𝑁 − 2 ) ) ∈ ( ( 𝑁 − 2 ) ClWWalksN 𝐺 ) )