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 W cyclShift N ClWWalks G

Proof

Step Hyp Ref Expression
1 oveq2 N = W W cyclShift N = W cyclShift W
2 eqid Vtx G = Vtx G
3 2 clwwlkbp W ClWWalks G G V W Word Vtx G W
4 3 simp2d W ClWWalks G W Word Vtx G
5 cshwn W Word Vtx G W cyclShift W = W
6 4 5 syl W ClWWalks G W cyclShift W = W
7 6 adantr W ClWWalks G N 0 W W cyclShift W = W
8 1 7 sylan9eq N = W W ClWWalks G N 0 W W cyclShift N = 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 W cyclShift N 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 syl5bir 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 W cyclShift N ClWWalks G
19 11 17 18 syl2anc ¬ N = W W ClWWalks G N 0 W W cyclShift N ClWWalks G
20 10 19 pm2.61ian W ClWWalks G N 0 W W cyclShift N ClWWalks G