Metamath Proof Explorer

Theorem clwwisshclwwsn

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, 15-Jun-2018) (Revised by AV, 29-Apr-2021)

Ref Expression
Assertion clwwisshclwwsn ⊢W∈ClWWalks⁡G∧N∈0…W→WcyclShiftN∈ClWWalks⁡G

Proof

Step Hyp Ref Expression
1 oveq2 ⊢N=W→WcyclShiftN=WcyclShiftW
2 eqid ⊢Vtx⁡G=Vtx⁡G
3 2 clwwlkbp ⊢W∈ClWWalks⁡G→G∈V∧W∈WordVtx⁡G∧W≠∅
4 3 simp2d ⊢W∈ClWWalks⁡G→W∈WordVtx⁡G
5 cshwn ⊢W∈WordVtx⁡G→WcyclShiftW=W
6 4 5 syl ⊢W∈ClWWalks⁡G→WcyclShiftW=W
7 6 adantr ⊢W∈ClWWalks⁡G∧N∈0…W→WcyclShiftW=W
8 1 7 sylan9eq ⊢N=W∧W∈ClWWalks⁡G∧N∈0…W→WcyclShiftN=W
9 simprl ⊢N=W∧W∈ClWWalks⁡G∧N∈0…W→W∈ClWWalks⁡G
10 8 9 eqeltrd ⊢N=W∧W∈ClWWalks⁡G∧N∈0…W→WcyclShiftN∈ClWWalks⁡G
11 simprl ⊢¬N=W∧W∈ClWWalks⁡G∧N∈0…W→W∈ClWWalks⁡G
12 df-ne ⊢N≠W↔¬N=W
13 fzofzim ⊢N≠W∧N∈0…W→N∈0..^W
14 13 expcom ⊢N∈0…W→N≠W→N∈0..^W
15 12 14 biimtrrid ⊢N∈0…W→¬N=W→N∈0..^W
16 15 adantl ⊢W∈ClWWalks⁡G∧N∈0…W→¬N=W→N∈0..^W
17 16 impcom ⊢¬N=W∧W∈ClWWalks⁡G∧N∈0…W→N∈0..^W
18 clwwisshclwws ⊢W∈ClWWalks⁡G∧N∈0..^W→WcyclShiftN∈ClWWalks⁡G
19 11 17 18 syl2anc ⊢¬N=W∧W∈ClWWalks⁡G∧N∈0…W→WcyclShiftN∈ClWWalks⁡G
20 10 19 pm2.61ian ⊢W∈ClWWalks⁡G∧N∈0…W→WcyclShiftN∈ClWWalks⁡G