Metamath Proof Explorer


Theorem upwlkwlk

Description: A simple walk is a walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 27-Feb-2021)

Ref Expression
Assertion upwlkwlk F UPWalks G P F Walks G P

Proof

Step Hyp Ref Expression
1 eqid Vtx G = Vtx G
2 eqid iEdg G = iEdg G
3 1 2 upwlkbprop F UPWalks G P G V F V P V
4 idd G V F V P V F Word dom iEdg G F Word dom iEdg G
5 idd G V F V P V P : 0 F Vtx G P : 0 F Vtx G
6 ifpprsnss iEdg G F k = P k P k + 1 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
7 6 a1i G V F V P V k 0 ..^ F iEdg G F k = P k P k + 1 if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
8 7 ralimdva G V F V P V k 0 ..^ F iEdg G F k = P k P k + 1 k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
9 4 5 8 3anim123d G V F V P V F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1 F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
10 1 2 isupwlk G V F V P V F UPWalks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F iEdg G F k = P k P k + 1
11 1 2 iswlk G V F V P V F Walks G P F Word dom iEdg G P : 0 F Vtx G k 0 ..^ F if- P k = P k + 1 iEdg G F k = P k P k P k + 1 iEdg G F k
12 9 10 11 3imtr4d G V F V P V F UPWalks G P F Walks G P
13 3 12 mpcom F UPWalks G P F Walks G P