Metamath Proof Explorer

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 
|- ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( N ClWWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
2 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
3 2eluzge1 
 |-  2 e. ( ZZ>= ` 1 )
4 subeluzsub 
 |-  ( ( N e. ZZ /\ 2 e. ( ZZ>= ` 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` ( N - 2 ) ) )
5 2 3 4 sylancl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) e. ( ZZ>= ` ( N - 2 ) ) )
6 1 5 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( ( N - 2 ) e. NN /\ ( N - 1 ) e. ( ZZ>= ` ( N - 2 ) ) ) )
7 6 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( N ClWWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( ( N - 2 ) e. NN /\ ( N - 1 ) e. ( ZZ>= ` ( N - 2 ) ) ) )
8 clwwlknwwlksn 
 |-  ( W e. ( N ClWWalksN G ) -> W e. ( ( N - 1 ) WWalksN G ) )
9 8 3ad2ant2 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( N ClWWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> W e. ( ( N - 1 ) WWalksN G ) )
10 simp3 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( N ClWWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W ` ( N - 2 ) ) = ( W ` 0 ) )
11 clwwlkinwwlk 
 |-  ( ( ( ( N - 2 ) e. NN /\ ( N - 1 ) e. ( ZZ>= ` ( N - 2 ) ) ) /\ W e. ( ( N - 1 ) WWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) )
12 7 9 10 11 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ W e. ( N ClWWalksN G ) /\ ( W ` ( N - 2 ) ) = ( W ` 0 ) ) -> ( W prefix ( N - 2 ) ) e. ( ( N - 2 ) ClWWalksN G ) )