Metamath Proof Explorer

Theorem clwwnisshclwwsn

Description: Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018) (Revised by AV, 29-Apr-2021) (Proof shortened by AV, 22-Mar-2022)

Ref Expression
Assertion clwwnisshclwwsn ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W cyclShift M ∈ N ClWWalksN G

Proof

Step Hyp Ref Expression
1 clwwlkclwwlkn ⊢ W ∈ N ClWWalksN G → W ∈ ClWWalks ⁡ G
2 clwwlknlen ⊢ W ∈ N ClWWalksN G → W = N
3 2 eqcomd ⊢ W ∈ N ClWWalksN G → N = W
4 3 oveq2d ⊢ W ∈ N ClWWalksN G → 0 … N = 0 … W
5 4 eleq2d ⊢ W ∈ N ClWWalksN G → M ∈ 0 … N ↔ M ∈ 0 … W
6 5 biimpa ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → M ∈ 0 … W
7 clwwisshclwwsn ⊢ W ∈ ClWWalks ⁡ G ∧ M ∈ 0 … W → W cyclShift M ∈ ClWWalks ⁡ G
8 1 6 7 syl2an2r ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W cyclShift M ∈ ClWWalks ⁡ G
9 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
10 9 clwwlknwrd ⊢ W ∈ N ClWWalksN G → W ∈ Word Vtx ⁡ G
11 elfzelz ⊢ M ∈ 0 … N → M ∈ ℤ
12 cshwlen ⊢ W ∈ Word Vtx ⁡ G ∧ M ∈ ℤ → W cyclShift M = W
13 10 11 12 syl2an ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W cyclShift M = W
14 2 adantr ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W = N
15 13 14 eqtrd ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W cyclShift M = N
16 isclwwlkn ⊢ W cyclShift M ∈ N ClWWalksN G ↔ W cyclShift M ∈ ClWWalks ⁡ G ∧ W cyclShift M = N
17 8 15 16 sylanbrc ⊢ W ∈ N ClWWalksN G ∧ M ∈ 0 … N → W cyclShift M ∈ N ClWWalksN G