Metamath Proof Explorer

Theorem isclwlkupgr

Description: Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 11-Apr-2021) (Revised by AV, 28-Oct-2021)

Ref Expression
Hypotheses isclwlke.v ⊢ V = Vtx ⁡ G
isclwlke.i ⊢ I = iEdg ⁡ G
Assertion isclwlkupgr ⊢ G ∈ UPGraph → F ClWalks ⁡ G P ↔ 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 isclwlk ⊢ F ClWalks ⁡ G P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F
4 1 2 upgriswlk ⊢ G ∈ UPGraph → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
5 4 anbi1d ⊢ G ∈ UPGraph → F Walks ⁡ G P ∧ 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
6 3an4anass ⊢ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ∧ 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
7 5 6 bitrdi ⊢ G ∈ UPGraph → F Walks ⁡ G P ∧ 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
8 3 7 bitrid ⊢ G ∈ UPGraph → F ClWalks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 ∧ P ⁡ 0 = P ⁡ F