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

Proof

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