Metamath Proof Explorer


Theorem upgrwlkcompim

Description: Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 14-Apr-2021)

Ref Expression
Hypotheses upgrwlkcompim.v V = Vtx G
upgrwlkcompim.i I = iEdg G
upgrwlkcompim.1 F = 1 st W
upgrwlkcompim.2 P = 2 nd W
Assertion upgrwlkcompim G UPGraph W Walks G F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1

Proof

Step Hyp Ref Expression
1 upgrwlkcompim.v V = Vtx G
2 upgrwlkcompim.i I = iEdg G
3 upgrwlkcompim.1 F = 1 st W
4 upgrwlkcompim.2 P = 2 nd W
5 wlkcpr W Walks G 1 st W Walks G 2 nd W
6 3 4 breq12i F Walks G P 1 st W Walks G 2 nd W
7 5 6 bitr4i W Walks G F Walks G P
8 1 2 upgriswlk G UPGraph F Walks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
9 8 biimpd G UPGraph F Walks G P F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
10 7 9 syl5bi G UPGraph W Walks G F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1
11 10 imp G UPGraph W Walks G F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1