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 ) )