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

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