Metamath Proof Explorer

Theorem wlkcompim

Description: Implications for the properties of the components of a walk. (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 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

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 elfvex ⊢ W ∈ Walks ⁡ G → G ∈ V
6 wlkcpr ⊢ W ∈ Walks ⁡ G ↔ 1 st ⁡ W Walks ⁡ G 2 nd ⁡ W
7 wlkvv ⊢ 1 st ⁡ W Walks ⁡ G 2 nd ⁡ W → W ∈ V × V
8 6 7 sylbi ⊢ W ∈ Walks ⁡ G → W ∈ V × V
9 1 2 3 4 wlkcomp ⊢ G ∈ V ∧ W ∈ V × V → 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
10 9 biimpcd ⊢ W ∈ Walks ⁡ G → G ∈ V ∧ W ∈ V × V → 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
11 5 8 10 mp2and ⊢ 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