Metamath Proof Explorer

Theorem clwwlknp

Description: Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018) (Revised by AV, 24-Apr-2021) (Proof shortened by AV, 23-Mar-2022)

Ref Expression
Hypotheses isclwwlknx.v ⊢ V = Vtx ⁡ G
isclwwlknx.e ⊢ E = Edg ⁡ G
Assertion clwwlknp ⊢ W ∈ N ClWWalksN G → W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E

Proof

Step Hyp Ref Expression
1 isclwwlknx.v ⊢ V = Vtx ⁡ G
2 isclwwlknx.e ⊢ E = Edg ⁡ G
3 1 clwwlknbp ⊢ W ∈ N ClWWalksN G → W ∈ Word V ∧ W = N
4 simpr ⊢ W ∈ N ClWWalksN G ∧ W ∈ Word V ∧ W = N → W ∈ Word V ∧ W = N
5 clwwlknnn ⊢ W ∈ N ClWWalksN G → N ∈ ℕ
6 1 2 isclwwlknx ⊢ N ∈ ℕ → W ∈ N ClWWalksN G ↔ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N
7 3simpc ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
8 7 adantr ⊢ W ∈ Word V ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ∧ W = N → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
9 6 8 syl6bi ⊢ N ∈ ℕ → W ∈ N ClWWalksN G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
10 5 9 mpcom ⊢ W ∈ N ClWWalksN G → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
11 10 adantr ⊢ W ∈ N ClWWalksN G ∧ W ∈ Word V ∧ W = N → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
12 oveq1 ⊢ W = N → W − 1 = N − 1
13 12 oveq2d ⊢ W = N → 0 ..^ W − 1 = 0 ..^ N − 1
14 13 raleqdv ⊢ W = N → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ↔ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E
15 14 anbi1d ⊢ W = N → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
16 15 ad2antll ⊢ W ∈ N ClWWalksN G ∧ W ∈ Word V ∧ W = N → ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
17 11 16 mpbid ⊢ W ∈ N ClWWalksN G ∧ W ∈ Word V ∧ W = N → ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
18 4 17 jca ⊢ W ∈ N ClWWalksN G ∧ W ∈ Word V ∧ W = N → W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
19 3 18 mpdan ⊢ W ∈ N ClWWalksN G → W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
20 3anass ⊢ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E
21 19 20 sylibr ⊢ W ∈ N ClWWalksN G → W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N − 1 W ⁡ i W ⁡ i + 1 ∈ E ∧ lastS ⁡ W W ⁡ 0 ∈ E