Metamath Proof Explorer

Theorem clwwlknwwlksn

Description: A word representing a closed walk of length N also represents a walk of length N - 1 . The walk is one edge shorter than the closed walk, because the last edge connecting the last with the first vertex is missing. For example, if <" a b c "> e. ( 3 ClWWalksN G ) represents a closed walk "abca" of length 3, then <" a b c "> e. ( 2 WWalksN G ) represents a walk "abc" (not closed if a =/= c ) of length 2, and <" a b c a "> e. ( 3 WWalksN G ) represents also a closed walk "abca" of length 3. (Contributed by AV, 24-Jan-2022) (Revised by AV, 22-Mar-2022)

Ref Expression
Assertion clwwlknwwlksn ⊢ W ∈ N ClWWalksN G → W ∈ N − 1 WWalksN G

Proof

Step Hyp Ref Expression
1 clwwlknnn ⊢ W ∈ N ClWWalksN G → N ∈ ℕ
2 idd ⊢ N ∈ ℕ → W ∈ Word Vtx ⁡ G → W ∈ Word Vtx ⁡ G
3 idd ⊢ N ∈ ℕ → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G
4 nncn ⊢ N ∈ ℕ → N ∈ ℂ
5 npcan1 ⊢ N ∈ ℂ → N - 1 + 1 = N
6 4 5 syl ⊢ N ∈ ℕ → N - 1 + 1 = N
7 6 eqcomd ⊢ N ∈ ℕ → N = N - 1 + 1
8 7 eqeq2d ⊢ N ∈ ℕ → W = N ↔ W = N - 1 + 1
9 8 biimpd ⊢ N ∈ ℕ → W = N → W = N - 1 + 1
10 2 3 9 3anim123d ⊢ N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
11 10 com12 ⊢ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N → N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
12 11 3exp ⊢ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → W = N → N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
13 12 a1dd ⊢ W ∈ Word Vtx ⁡ G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = N → N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
14 13 adantr ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G → lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G → W = N → N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
15 14 3imp1 ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = N → N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
16 15 com12 ⊢ N ∈ ℕ → W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = N → W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
17 isclwwlkn ⊢ W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
18 17 a1i ⊢ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ ClWWalks ⁡ G ∧ W = N
19 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
20 eqid ⊢ Edg ⁡ G = Edg ⁡ G
21 19 20 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
22 21 anbi1i ⊢ W ∈ ClWWalks ⁡ G ∧ W = N ↔ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = N
23 18 22 bitrdi ⊢ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G ∧ W = N
24 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
25 19 20 iswwlksnx ⊢ N − 1 ∈ ℕ 0 → W ∈ N − 1 WWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
26 24 25 syl ⊢ N ∈ ℕ → W ∈ N − 1 WWalksN G ↔ W ∈ Word Vtx ⁡ G ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ W = N - 1 + 1
27 16 23 26 3imtr4d ⊢ N ∈ ℕ → W ∈ N ClWWalksN G → W ∈ N − 1 WWalksN G
28 1 27 mpcom ⊢ W ∈ N ClWWalksN G → W ∈ N − 1 WWalksN G