Metamath Proof Explorer


Theorem wwlkbp

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 V=VtxG
Assertion wwlkbp WWWalksGGVWWordV

Proof

Step Hyp Ref Expression
1 wwlkbp.v V=VtxG
2 elfvex WWWalksGGV
3 eqid EdgG=EdgG
4 1 3 iswwlks WWWalksGWWWordVi0..^W1WiWi+1EdgG
5 4 simp2bi WWWalksGWWordV
6 2 5 jca WWWalksGGVWWordV