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 ..^ W W ⁡ i = T ⁡ i

Proof

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