Metamath Proof Explorer

Theorem wwlkseq

Description: Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018) (Revised by AV, 16-Apr-2021)

Ref Expression
Assertion wwlkseq ⊢W∈WWalks⁡G∧T∈WWalks⁡G→W=T↔W=T∧∀i∈0..^WW⁡i=T⁡i

Proof

Step Hyp Ref Expression
1 eqid ⊢Vtx⁡G=Vtx⁡G
2 1 wwlkbp ⊢W∈WWalks⁡G→G∈V∧W∈WordVtx⁡G
3 2 simprd ⊢W∈WWalks⁡G→W∈WordVtx⁡G
4 1 wwlkbp ⊢T∈WWalks⁡G→G∈V∧T∈WordVtx⁡G
5 4 simprd ⊢T∈WWalks⁡G→T∈WordVtx⁡G
6 eqwrd ⊢W∈WordVtx⁡G∧T∈WordVtx⁡G→W=T↔W=T∧∀i∈0..^WW⁡i=T⁡i
7 3 5 6 syl2an ⊢W∈WWalks⁡G∧T∈WWalks⁡G→W=T↔W=T∧∀i∈0..^WW⁡i=T⁡i