Description: Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018) (Revised by AV, 9-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wwlkbp.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| Assertion | wwlkbp | ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wwlkbp.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | elfvex | ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → 𝐺 ∈ V ) | |
| 3 | eqid | ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) | |
| 4 | 1 3 | iswwlks | ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) ↔ ( 𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑊 ) − 1 ) ) { ( 𝑊 ‘ 𝑖 ) , ( 𝑊 ‘ ( 𝑖 + 1 ) ) } ∈ ( Edg ‘ 𝐺 ) ) ) |
| 5 | 4 | simp2bi | ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → 𝑊 ∈ Word 𝑉 ) |
| 6 | 2 5 | jca | ⊢ ( 𝑊 ∈ ( WWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉 ) ) |