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 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 → 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