Metamath Proof Explorer

Theorem clwwlkbp

Description: Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Hypothesis clwwlkbp.v ⊢ V = Vtx ⁡ G
Assertion clwwlkbp ⊢ W ∈ ClWWalks ⁡ G → G ∈ V ∧ W ∈ Word V ∧ W ≠ ∅

Proof

Step Hyp Ref Expression
1 clwwlkbp.v ⊢ V = Vtx ⁡ G
2 elfvex ⊢ W ∈ ClWWalks ⁡ G → G ∈ V
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 isclwwlk ⊢ W ∈ ClWWalks ⁡ G ↔ W ∈ Word V ∧ W ≠ ∅ ∧ ∀ i ∈ 0 ..^ W − 1 W ⁡ i W ⁡ i + 1 ∈ Edg ⁡ G ∧ lastS ⁡ W W ⁡ 0 ∈ Edg ⁡ G
5 4 simp1bi ⊢ W ∈ ClWWalks ⁡ G → W ∈ Word V ∧ W ≠ ∅
6 3anass ⊢ G ∈ V ∧ W ∈ Word V ∧ W ≠ ∅ ↔ G ∈ V ∧ W ∈ Word V ∧ W ≠ ∅
7 2 5 6 sylanbrc ⊢ W ∈ ClWWalks ⁡ G → G ∈ V ∧ W ∈ Word V ∧ W ≠ ∅