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∈WordV∧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∈WordV∧W≠∅∧∀i∈0..^W−1W⁡iW⁡i+1∈Edg⁡G∧lastS⁡WW⁡0∈Edg⁡G
5 4 simp1bi ⊢W∈ClWWalks⁡G→W∈WordV∧W≠∅
6 3anass ⊢G∈V∧W∈WordV∧W≠∅↔G∈V∧W∈WordV∧W≠∅
7 2 5 6 sylanbrc ⊢W∈ClWWalks⁡G→G∈V∧W∈WordV∧W≠∅