Metamath Proof Explorer


Theorem wlkcompim

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

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

Proof

Step Hyp Ref Expression
1 wlkcomp.v V = Vtx G
2 wlkcomp.i I = iEdg G
3 wlkcomp.1 F = 1 st W
4 wlkcomp.2 P = 2 nd W
5 elfvex W Walks G G V
6 wlkcpr W Walks G 1 st W Walks G 2 nd W
7 wlkvv 1 st W Walks G 2 nd W W V × V
8 6 7 sylbi W Walks G W V × V
9 1 2 3 4 wlkcomp G V W V × V W Walks G F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k
10 9 biimpcd W Walks G G V W V × V F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k
11 5 8 10 mp2and W Walks G F Word dom I P : 0 F V k 0 ..^ F if- P k = P k + 1 I F k = P k P k P k + 1 I F k