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 = 1 st ⁡ W
clwlkcomp.2 ⊢ P = 2 nd ⁡ W
Assertion 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

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 elfvex ⊢ W ∈ ClWalks ⁡ G → G ∈ V
6 clwlks ⊢ ClWalks ⁡ G = f g | f Walks ⁡ G g ∧ g ⁡ 0 = g ⁡ f
7 6 a1i ⊢ G ∈ V → ClWalks ⁡ G = f g | f Walks ⁡ G g ∧ g ⁡ 0 = g ⁡ f
8 7 eleq2d ⊢ G ∈ V → W ∈ ClWalks ⁡ G ↔ W ∈ f g | f Walks ⁡ G g ∧ g ⁡ 0 = g ⁡ f
9 elopaelxp ⊢ W ∈ f g | f Walks ⁡ G g ∧ g ⁡ 0 = g ⁡ f → W ∈ V × V
10 9 anim2i ⊢ G ∈ V ∧ W ∈ f g | f Walks ⁡ G g ∧ g ⁡ 0 = g ⁡ f → G ∈ V ∧ W ∈ V × V
11 10 ex ⊢ G ∈ V → W ∈ f g | f Walks ⁡ G g ∧ 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 ∈ 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
15 13 14 syl ⊢ W ∈ ClWalks ⁡ G → 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
16 15 ibi ⊢ 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