Metamath Proof Explorer

Theorem clwwlkgt0

Description: There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018) (Revised by AV, 24-Apr-2021)

Ref Expression
Assertion clwwlkgt0 ⊢ W ∈ ClWWalks ⁡ G → 0 < W

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 hashgt0 ⊢ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ → 0 < W
4 3 3adant1 ⊢ G ∈ V ∧ W ∈ Word Vtx ⁡ G ∧ W ≠ ∅ → 0 < W
5 2 4 syl ⊢ W ∈ ClWWalks ⁡ G → 0 < W