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 ( ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( 𝑊 cyclShift 𝑁 ) ∈ ( ClWWalks ‘ 𝐺 ) )

Proof

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