Metamath Proof Explorer

Theorem upwlkwlk

Description: A simple walk is a walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 27-Feb-2021)

Ref Expression
Assertion upwlkwlk ⊢ F UPWalks ⁡ G P → F Walks ⁡ G P

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
3 1 2 upwlkbprop ⊢ F UPWalks ⁡ G P → G ∈ V ∧ F ∈ V ∧ P ∈ V
4 idd ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ Word dom ⁡ iEdg ⁡ G → F ∈ Word dom ⁡ iEdg ⁡ G
5 idd ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → P : 0 … F ⟶ Vtx ⁡ G → P : 0 … F ⟶ Vtx ⁡ G
6 ifpprsnss ⊢ iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
7 6 a1i ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V ∧ k ∈ 0 ..^ F → iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
8 7 ralimdva ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
9 4 5 8 3anim123d ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1 → F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
10 1 2 isupwlk ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F UPWalks ⁡ G P ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
11 1 2 iswlk ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ iEdg ⁡ G ∧ P : 0 … F ⟶ Vtx ⁡ G ∧ ∀ k ∈ 0 ..^ F if- P ⁡ k = P ⁡ k + 1 iEdg ⁡ G ⁡ F ⁡ k = P ⁡ k P ⁡ k P ⁡ k + 1 ⊆ iEdg ⁡ G ⁡ F ⁡ k
12 9 10 11 3imtr4d ⊢ G ∈ V ∧ F ∈ V ∧ P ∈ V → F UPWalks ⁡ G P → F Walks ⁡ G P
13 3 12 mpcom ⊢ F UPWalks ⁡ G P → F Walks ⁡ G P