Metamath Proof Explorer

Theorem wlkelwrd

Description: The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Hypotheses wlkcomp.v ⊢ V = Vtx ⁡ G
wlkcomp.i ⊢ I = iEdg ⁡ G
wlkcomp.1 ⊢ F = 1 st ⁡ W
wlkcomp.2 ⊢ P = 2 nd ⁡ W
Assertion wlkelwrd ⊢ W ∈ Walks ⁡ G → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V

Proof

Step Hyp Ref Expression
1 wlkcomp.v ⊢ V = Vtx ⁡ G
2 wlkcomp.i ⊢ I = iEdg ⁡ G
3 wlkcomp.1 ⊢ F = 1 st ⁡ W
4 wlkcomp.2 ⊢ P = 2 nd ⁡ W
5 1 2 3 4 wlkcompim ⊢ W ∈ Walks ⁡ G → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
6 3simpa ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V
7 5 6 syl ⊢ W ∈ Walks ⁡ G → F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V