Metamath Proof Explorer


Theorem clwlkcomp

Description: A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 17-Feb-2021)

Ref Expression
Hypotheses isclwlke.v V = Vtx G
isclwlke.i I = iEdg G
clwlkcomp.1 F = 1 st W
clwlkcomp.2 P = 2 nd W
Assertion clwlkcomp G X W S × T W ClWalks 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 P 0 = P F

Proof

Step Hyp Ref Expression
1 isclwlke.v V = Vtx G
2 isclwlke.i I = iEdg G
3 clwlkcomp.1 F = 1 st W
4 clwlkcomp.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 ClWalks G F P ClWalks G
11 df-br F ClWalks G P F P ClWalks G
12 10 11 bitr4di W S × T W ClWalks G F ClWalks G P
13 1 2 isclwlke G X F ClWalks 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 P 0 = P F
14 12 13 sylan9bbr G X W S × T W ClWalks 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 P 0 = P F