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 ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 0 < ( ♯ ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 1 clwwlkbp ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) )
3 hashgt0 ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) → 0 < ( ♯ ‘ 𝑊 ) )
4 3 3adant1 ( ( 𝐺 ∈ V ∧ 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑊 ≠ ∅ ) → 0 < ( ♯ ‘ 𝑊 ) )
5 2 4 syl ( 𝑊 ∈ ( ClWWalks ‘ 𝐺 ) → 0 < ( ♯ ‘ 𝑊 ) )