Metamath Proof Explorer

Theorem wlkd

Description: Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses wlkd.p ⊢ φ → P ∈ Word V
wlkd.f ⊢ φ → F ∈ Word V
wlkd.l ⊢ φ → P = F + 1
wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
wlkd.n ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
wlkd.g ⊢ φ → G ∈ W
wlkd.v ⊢ V = Vtx ⁡ G
wlkd.i ⊢ I = iEdg ⁡ G
wlkd.a ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V
Assertion wlkd ⊢ φ → F Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 wlkd.p ⊢ φ → P ∈ Word V
2 wlkd.f ⊢ φ → F ∈ Word V
3 wlkd.l ⊢ φ → P = F + 1
4 wlkd.e ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
5 wlkd.n ⊢ φ → ∀ k ∈ 0 ..^ F P ⁡ k ≠ P ⁡ k + 1
6 wlkd.g ⊢ φ → G ∈ W
7 wlkd.v ⊢ V = Vtx ⁡ G
8 wlkd.i ⊢ I = iEdg ⁡ G
9 wlkd.a ⊢ φ → ∀ k ∈ 0 … F P ⁡ k ∈ V
10 1 2 3 4 wlkdlem3 ⊢ φ → F ∈ Word dom ⁡ I
11 1 2 3 9 wlkdlem1 ⊢ φ → P : 0 … F ⟶ V
12 1 2 3 4 5 wlkdlem4 ⊢ φ → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k
13 7 8 iswlk ⊢ G ∈ W ∧ F ∈ Word V ∧ P ∈ Word V → F Walks ⁡ G P ↔ 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
14 6 2 1 13 syl3anc ⊢ φ → F Walks ⁡ G P ↔ 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
15 10 11 12 14 mpbir3and ⊢ φ → F Walks ⁡ G P