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

Metamath Proof Explorer

Theorem upgrwlkvtxedg

Description: The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018) (Revised by AV, 2-Jan-2021)

Ref Expression
Hypothesis wlkvtxedg.e ⊢ E = Edg ⁡ G
Assertion upgrwlkvtxedg ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E

Proof

Step Hyp Ref Expression
1 wlkvtxedg.e ⊢ E = Edg ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 2 3 upgriswlk ⊢ G ∈ UPGraph → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
5 3 1 upgredginwlk ⊢ G ∈ UPGraph ∧ F ∈ Word dom ⁡ iEdg ⁡ G → k ∈ 0 ..^ F → iEdg ⁡ G ⁡ F ⁡ k ∈ E
6 5 ancoms ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → k ∈ 0 ..^ F → iEdg ⁡ G ⁡ F ⁡ k ∈ E
7 6 imp ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph ∧ k ∈ 0 ..^ F → iEdg ⁡ G ⁡ F ⁡ k ∈ E
8 eleq1 ⊢ P ⁡ k P ⁡ k + 1 = iEdg ⁡ G ⁡ F ⁡ k → P ⁡ k P ⁡ k + 1 ∈ E ↔ iEdg ⁡ G ⁡ F ⁡ k ∈ E
9 8 eqcoms ⊢ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → P ⁡ k P ⁡ k + 1 ∈ E ↔ iEdg ⁡ G ⁡ F ⁡ k ∈ E
10 7 9 syl5ibrcom ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph ∧ k ∈ 0 ..^ F → iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → P ⁡ k P ⁡ k + 1 ∈ E
11 10 ralimdva ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E
12 11 impancom ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → G ∈ UPGraph → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E
13 12 3adant2 ⊢ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → G ∈ UPGraph → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E
14 13 com12 ⊢ G ∈ UPGraph → F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E
15 4 14 sylbid ⊢ G ∈ UPGraph → F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E
16 15 imp ⊢ G ∈ UPGraph ∧ F Walks ⁡ G P → ∀ k ∈ 0 ..^ F P ⁡ k P ⁡ k + 1 ∈ E