Metamath Proof Explorer


Theorem upwlkbprop

Description: Basic properties of a simple walk. (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 29-Dec-2020)

Ref Expression
Hypotheses upwlksfval.v V = Vtx G
upwlksfval.i I = iEdg G
Assertion upwlkbprop F UPWalks G P G V F V P V

Proof

Step Hyp Ref Expression
1 upwlksfval.v V = Vtx G
2 upwlksfval.i I = iEdg G
3 1 2 upwlksfval G V UPWalks G = f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1
4 3 breqd G V F UPWalks G P F f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 P
5 brabv F f p | f Word dom I p : 0 f V k 0 ..^ f I f k = p k p k + 1 P F V P V
6 4 5 syl6bi G V F UPWalks G P F V P V
7 6 imdistani G V F UPWalks G P G V F V P V
8 3anass G V F V P V G V F V P V
9 7 8 sylibr G V F UPWalks G P G V F V P V
10 9 ex G V F UPWalks G P G V F V P V
11 fvprc ¬ G V UPWalks G =
12 breq UPWalks G = F UPWalks G P F P
13 br0 ¬ F P
14 13 pm2.21i F P G V F V P V
15 12 14 syl6bi UPWalks G = F UPWalks G P G V F V P V
16 11 15 syl ¬ G V F UPWalks G P G V F V P V
17 10 16 pm2.61i F UPWalks G P G V F V P V