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 < ( ♯ ‘ 𝑊 ) ) |
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 < ( ♯ ‘ 𝑊 ) ) |