Metamath Proof Explorer

Theorem clwlkcompim

Description: Implications for the properties of the components of a closed walk. (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=1st⁡W
clwlkcomp.2 ⊢P=2nd⁡W
Assertion clwlkcompim ⊢W∈ClWalks⁡G→F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡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=1st⁡W
4 clwlkcomp.2 ⊢P=2nd⁡W
5 elfvex ⊢W∈ClWalks⁡G→G∈V
6 clwlks ⊢ClWalks⁡G=fg|fWalks⁡Gg∧g⁡0=g⁡f
7 6 a1i ⊢G∈V→ClWalks⁡G=fg|fWalks⁡Gg∧g⁡0=g⁡f
8 7 eleq2d ⊢G∈V→W∈ClWalks⁡G↔W∈fg|fWalks⁡Gg∧g⁡0=g⁡f
9 elopaelxp ⊢W∈fg|fWalks⁡Gg∧g⁡0=g⁡f→W∈V×V
10 9 anim2i ⊢G∈V∧W∈fg|fWalks⁡Gg∧g⁡0=g⁡f→G∈V∧W∈V×V
11 10 ex ⊢G∈V→W∈fg|fWalks⁡Gg∧g⁡0=g⁡f→G∈V∧W∈V×V
12 8 11 sylbid ⊢G∈V→W∈ClWalks⁡G→G∈V∧W∈V×V
13 5 12 mpcom ⊢W∈ClWalks⁡G→G∈V∧W∈V×V
14 1 2 3 4 clwlkcomp ⊢G∈V∧W∈V×V→W∈ClWalks⁡G↔F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k∧P⁡0=P⁡F
15 13 14 syl ⊢W∈ClWalks⁡G→W∈ClWalks⁡G↔F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k∧P⁡0=P⁡F
16 15 ibi ⊢W∈ClWalks⁡G→F∈Worddom⁡I∧P:0…F⟶V∧∀k∈0..^Fif-P⁡k=P⁡k+1I⁡F⁡k=P⁡kP⁡kP⁡k+1⊆I⁡F⁡k∧P⁡0=P⁡F