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