Metamath Proof Explorer

Theorem clwwisshclwws

Description: Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Mar-2018) (Revised by AV, 28-Apr-2021)

Ref Expression
Assertion clwwisshclwws 
|- ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 clwwlkbp 
 |-  ( W e. ( ClWWalks ` G ) -> ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) )
3 cshw0 
 |-  ( W e. Word ( Vtx ` G ) -> ( W cyclShift 0 ) = W )
4 3 3ad2ant2 
 |-  ( ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( W cyclShift 0 ) = W )
5 4 eleq1d 
 |-  ( ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( ( W cyclShift 0 ) e. ( ClWWalks ` G ) <-> W e. ( ClWWalks ` G ) ) )
6 5 biimprd 
 |-  ( ( G e. _V /\ W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( W e. ( ClWWalks ` G ) -> ( W cyclShift 0 ) e. ( ClWWalks ` G ) ) )
7 2 6 mpcom 
 |-  ( W e. ( ClWWalks ` G ) -> ( W cyclShift 0 ) e. ( ClWWalks ` G ) )
8 oveq2 
 |-  ( N = 0 -> ( W cyclShift N ) = ( W cyclShift 0 ) )
9 8 eleq1d 
 |-  ( N = 0 -> ( ( W cyclShift N ) e. ( ClWWalks ` G ) <-> ( W cyclShift 0 ) e. ( ClWWalks ` G ) ) )
10 7 9 syl5ibrcom 
 |-  ( W e. ( ClWWalks ` G ) -> ( N = 0 -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) )
11 10 adantr 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( N = 0 -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) )
12 fzo1fzo0n0 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) <-> ( N e. ( 0 ..^ ( # ` W ) ) /\ N =/= 0 ) )
13 cshwcl 
 |-  ( W e. Word ( Vtx ` G ) -> ( W cyclShift N ) e. Word ( Vtx ` G ) )
14 13 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( W cyclShift N ) e. Word ( Vtx ` G ) )
15 14 3ad2ant1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( W cyclShift N ) e. Word ( Vtx ` G ) )
16 15 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. Word ( Vtx ` G ) )
17 simpl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> W e. Word ( Vtx ` G ) )
18 elfzoelz 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> N e. ZZ )
19 cshwlen 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ZZ ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
20 17 18 19 syl2an 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` ( W cyclShift N ) ) = ( # ` W ) )
21 hasheq0 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` W ) = 0 <-> W = (/) ) )
22 21 bicomd 
 |-  ( W e. Word ( Vtx ` G ) -> ( W = (/) <-> ( # ` W ) = 0 ) )
23 22 necon3bid 
 |-  ( W e. Word ( Vtx ` G ) -> ( W =/= (/) <-> ( # ` W ) =/= 0 ) )
24 23 biimpa 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( # ` W ) =/= 0 )
25 24 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` W ) =/= 0 )
26 20 25 eqnetrd 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( # ` ( W cyclShift N ) ) =/= 0 )
27 14 adantr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. Word ( Vtx ` G ) )
28 hasheq0 
 |-  ( ( W cyclShift N ) e. Word ( Vtx ` G ) -> ( ( # ` ( W cyclShift N ) ) = 0 <-> ( W cyclShift N ) = (/) ) )
29 27 28 syl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( # ` ( W cyclShift N ) ) = 0 <-> ( W cyclShift N ) = (/) ) )
30 29 necon3bid 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( # ` ( W cyclShift N ) ) =/= 0 <-> ( W cyclShift N ) =/= (/) ) )
31 26 30 mpbid 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) =/= (/) )
32 31 3ad2antl1 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) =/= (/) )
33 16 32 jca 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) e. Word ( Vtx ` G ) /\ ( W cyclShift N ) =/= (/) ) )
34 17 3ad2ant1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> W e. Word ( Vtx ` G ) )
35 34 anim1i 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) )
36 3simpc 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
37 36 adantr 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
38 clwwisshclwwslem 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ( Edg ` G ) ) )
39 35 37 38 sylc 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ( Edg ` G ) )
40 elfzofz 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> N e. ( 1 ... ( # ` W ) ) )
41 lswcshw 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ... ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( W ` ( N - 1 ) ) )
42 40 41 sylan2 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( lastS ` ( W cyclShift N ) ) = ( W ` ( N - 1 ) ) )
43 fzo0ss1 
 |-  ( 1 ..^ ( # ` W ) ) C_ ( 0 ..^ ( # ` W ) )
44 43 sseli 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> N e. ( 0 ..^ ( # ` W ) ) )
45 cshwidx0 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) )
46 44 45 sylan2 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( W cyclShift N ) ` 0 ) = ( W ` N ) )
47 42 46 preq12d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } )
48 47 ex 
 |-  ( W e. Word ( Vtx ` G ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } ) )
49 48 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } ) )
50 49 3ad2ant1 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } ) )
51 50 imp 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } )
52 elfzo1elm1fzo0 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> ( N - 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
53 52 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( N - 1 ) e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
54 fveq2 
 |-  ( i = ( N - 1 ) -> ( W ` i ) = ( W ` ( N - 1 ) ) )
55 54 adantl 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ i = ( N - 1 ) ) -> ( W ` i ) = ( W ` ( N - 1 ) ) )
56 fvoveq1 
 |-  ( i = ( N - 1 ) -> ( W ` ( i + 1 ) ) = ( W ` ( ( N - 1 ) + 1 ) ) )
57 18 zcnd 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> N e. CC )
58 57 adantl 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> N e. CC )
59 1cnd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> 1 e. CC )
60 58 59 npcand 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( N - 1 ) + 1 ) = N )
61 60 fveq2d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( W ` ( ( N - 1 ) + 1 ) ) = ( W ` N ) )
62 56 61 sylan9eqr 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ i = ( N - 1 ) ) -> ( W ` ( i + 1 ) ) = ( W ` N ) )
63 55 62 preq12d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ i = ( N - 1 ) ) -> { ( W ` i ) , ( W ` ( i + 1 ) ) } = { ( W ` ( N - 1 ) ) , ( W ` N ) } )
64 63 eleq1d 
 |-  ( ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) /\ i = ( N - 1 ) ) -> ( { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) <-> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) )
65 53 64 rspcdv 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) )
66 65 a1d 
 |-  ( ( W e. Word ( Vtx ` G ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) )
67 66 ex 
 |-  ( W e. Word ( Vtx ` G ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) ) )
68 67 adantr 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) ) )
69 68 com24 
 |-  ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) -> ( A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) -> ( { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) -> ( N e. ( 1 ..^ ( # ` W ) ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) ) ) ) )
70 69 3imp1 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( W ` ( N - 1 ) ) , ( W ` N ) } e. ( Edg ` G ) )
71 51 70 eqeltrd 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } e. ( Edg ` G ) )
72 33 39 71 3jca 
 |-  ( ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) /\ N e. ( 1 ..^ ( # ` W ) ) ) -> ( ( ( W cyclShift N ) e. Word ( Vtx ` G ) /\ ( W cyclShift N ) =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } e. ( Edg ` G ) ) )
73 72 expcom 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> ( ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) -> ( ( ( W cyclShift N ) e. Word ( Vtx ` G ) /\ ( W cyclShift N ) =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } e. ( Edg ` G ) ) ) )
74 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
75 1 74 isclwwlk 
 |-  ( W e. ( ClWWalks ` G ) <-> ( ( W e. Word ( Vtx ` G ) /\ W =/= (/) ) /\ A. i e. ( 0 ..^ ( ( # ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` W ) , ( W ` 0 ) } e. ( Edg ` G ) ) )
76 1 74 isclwwlk 
 |-  ( ( W cyclShift N ) e. ( ClWWalks ` G ) <-> ( ( ( W cyclShift N ) e. Word ( Vtx ` G ) /\ ( W cyclShift N ) =/= (/) ) /\ A. j e. ( 0 ..^ ( ( # ` ( W cyclShift N ) ) - 1 ) ) { ( ( W cyclShift N ) ` j ) , ( ( W cyclShift N ) ` ( j + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` ( W cyclShift N ) ) , ( ( W cyclShift N ) ` 0 ) } e. ( Edg ` G ) ) )
77 73 75 76 3imtr4g 
 |-  ( N e. ( 1 ..^ ( # ` W ) ) -> ( W e. ( ClWWalks ` G ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) )
78 12 77 sylbir 
 |-  ( ( N e. ( 0 ..^ ( # ` W ) ) /\ N =/= 0 ) -> ( W e. ( ClWWalks ` G ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) )
79 78 expcom 
 |-  ( N =/= 0 -> ( N e. ( 0 ..^ ( # ` W ) ) -> ( W e. ( ClWWalks ` G ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) ) )
80 79 com13 
 |-  ( W e. ( ClWWalks ` G ) -> ( N e. ( 0 ..^ ( # ` W ) ) -> ( N =/= 0 -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) ) )
81 80 imp 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( N =/= 0 -> ( W cyclShift N ) e. ( ClWWalks ` G ) ) )
82 11 81 pm2.61dne 
 |-  ( ( W e. ( ClWWalks ` G ) /\ N e. ( 0 ..^ ( # ` W ) ) ) -> ( W cyclShift N ) e. ( ClWWalks ` G ) )