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