Metamath Proof Explorer


Theorem upgrclwlkcompim

Description: Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 2-May-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 upgrclwlkcompim G UPGraph W ClWalks G F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 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 1 2 3 4 clwlkcompim 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
6 5 adantl G UPGraph 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
7 simprl G UPGraph 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 F Word dom I P : 0 F V
8 clwlkwlk W ClWalks G W Walks G
9 1 2 3 4 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
10 9 simp3d G UPGraph W Walks G k 0 ..^ F I F k = P k P k + 1
11 8 10 sylan2 G UPGraph W ClWalks G k 0 ..^ F I F k = P k P k + 1
12 11 adantr G UPGraph 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 k 0 ..^ F I F k = P k P k + 1
13 simprrr G UPGraph 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 P 0 = P F
14 7 12 13 3jca G UPGraph 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 F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 P 0 = P F
15 6 14 mpdan G UPGraph W ClWalks G F Word dom I P : 0 F V k 0 ..^ F I F k = P k P k + 1 P 0 = P F