This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isclwlke

Description: Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 16-Feb-2021)

Ref Expression
Hypotheses isclwlke.v ⊢ V = Vtx ⁡ G
isclwlke.i ⊢ I = iEdg ⁡ G
Assertion 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

Proof

Step Hyp Ref Expression
1 isclwlke.v ⊢ V = Vtx ⁡ G
2 isclwlke.i ⊢ I = iEdg ⁡ G
3 isclwlk ⊢ F ClWalks ⁡ G P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F
4 1 2 iswlkg ⊢ G ∈ X → 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
5 df-3an ⊢ 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 ↔ 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
6 4 5 bitrdi ⊢ G ∈ X → 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
7 6 anbi1d ⊢ G ∈ X → F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F ↔ 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
8 anass ⊢ 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 if- P ⁡ k = P ⁡ k + 1 I ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ I ⁡ F ⁡ k ∧ P ⁡ 0 = P ⁡ F
9 7 8 bitrdi ⊢ G ∈ X → F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F ↔ 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
10 3 9 bitrid ⊢ 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