This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwwnisshclwwsn

Description: Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018) (Revised by AV, 29-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Assertion clwwnisshclwwsn 
|- ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( W cyclShift M ) e. ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlkclwwlkn 
 |-  ( W e. ( N ClWWalksN G ) -> W e. ( ClWWalks ` G ) )
2 clwwlknlen 
 |-  ( W e. ( N ClWWalksN G ) -> ( # ` W ) = N )
3 2 eqcomd 
 |-  ( W e. ( N ClWWalksN G ) -> N = ( # ` W ) )
4 3 oveq2d 
 |-  ( W e. ( N ClWWalksN G ) -> ( 0 ... N ) = ( 0 ... ( # ` W ) ) )
5 4 eleq2d 
 |-  ( W e. ( N ClWWalksN G ) -> ( M e. ( 0 ... N ) <-> M e. ( 0 ... ( # ` W ) ) ) )
6 5 biimpa 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> M e. ( 0 ... ( # ` W ) ) )
7 clwwisshclwwsn 
 |-  ( ( W e. ( ClWWalks ` G ) /\ M e. ( 0 ... ( # ` W ) ) ) -> ( W cyclShift M ) e. ( ClWWalks ` G ) )
8 1 6 7 syl2an2r 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( W cyclShift M ) e. ( ClWWalks ` G ) )
9 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
10 9 clwwlknwrd 
 |-  ( W e. ( N ClWWalksN G ) -> W e. Word ( Vtx ` G ) )
11 elfzelz 
 |-  ( M e. ( 0 ... N ) -> M e. ZZ )
12 cshwlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ M e. ZZ ) -> ( # ` ( W cyclShift M ) ) = ( # ` W ) )
13 10 11 12 syl2an 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` ( W cyclShift M ) ) = ( # ` W ) )
14 2 adantr 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` W ) = N )
15 13 14 eqtrd 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( # ` ( W cyclShift M ) ) = N )
16 isclwwlkn 
 |-  ( ( W cyclShift M ) e. ( N ClWWalksN G ) <-> ( ( W cyclShift M ) e. ( ClWWalks ` G ) /\ ( # ` ( W cyclShift M ) ) = N ) )
17 8 15 16 sylanbrc 
 |-  ( ( W e. ( N ClWWalksN G ) /\ M e. ( 0 ... N ) ) -> ( W cyclShift M ) e. ( N ClWWalksN G ) )