This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkcomp

Description: A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-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 wlkcomp ⊢ G ∈ U ∧ W ∈ S × T → 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 3 eqcomi ⊢ 1 st ⁡ W = F
6 4 eqcomi ⊢ 2 nd ⁡ W = P
7 5 6 pm3.2i ⊢ 1 st ⁡ W = F ∧ 2 nd ⁡ W = P
8 eqop ⊢ W ∈ S × T → W = F P ↔ 1 st ⁡ W = F ∧ 2 nd ⁡ W = P
9 7 8 mpbiri ⊢ W ∈ S × T → W = F P
10 9 eleq1d ⊢ W ∈ S × T → W ∈ Walks ⁡ G ↔ F P ∈ Walks ⁡ G
11 df-br ⊢ F Walks ⁡ G P ↔ F P ∈ Walks ⁡ G
12 10 11 bitr4di ⊢ W ∈ S × T → W ∈ Walks ⁡ G ↔ F Walks ⁡ G P
13 1 2 iswlkg ⊢ G ∈ U → 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 12 13 sylan9bbr ⊢ G ∈ U ∧ W ∈ S × T → 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