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∈ClWWalks⁡G∧N∈0..^W→WcyclShiftN∈ClWWalks⁡G

Proof

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