Metamath Proof Explorer


Theorem wlkcomp

Description: A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018) (Revised by AV, 1-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 wlkcomp G U W S × T 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 3 eqcomi 1 st W = F
6 4 eqcomi 2 nd W = P
7 5 6 pm3.2i 1 st W = F 2 nd W = P
8 eqop W S × T W = F P 1 st W = F 2 nd W = P
9 7 8 mpbiri W S × T W = F P
10 9 eleq1d W S × T W Walks G F P Walks G
11 df-br F Walks G P F P Walks G
12 10 11 bitr4di W S × T W Walks G F Walks G P
13 1 2 iswlkg G U F Walks G P 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
14 12 13 sylan9bbr G U W S × T 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