Metamath Proof Explorer

Theorem upgrisupwlkALT

Description: Alternate proof of upgriswlk using the definition of UPGraph and related theorems. (Contributed by AV, 2-Jan-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses upgrisupwlkALT.v ⊢ V = Vtx ⁡ G
upgrisupwlkALT.i ⊢ I = iEdg ⁡ G
Assertion upgrisupwlkALT ⊢ G ∈ UPGraph ∧ F ∈ U ∧ P ∈ Z → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1

Proof

Step Hyp Ref Expression
1 upgrisupwlkALT.v ⊢ V = Vtx ⁡ G
2 upgrisupwlkALT.i ⊢ I = iEdg ⁡ G
3 upgrwlkupwlkb ⊢ G ∈ UPGraph → F Walks ⁡ G P ↔ F UPWalks ⁡ G P
4 3 3ad2ant1 ⊢ G ∈ UPGraph ∧ F ∈ U ∧ P ∈ Z → F Walks ⁡ G P ↔ F UPWalks ⁡ G P
5 1 2 isupwlk ⊢ G ∈ UPGraph ∧ F ∈ U ∧ P ∈ Z → F UPWalks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1
6 4 5 bitrd ⊢ G ∈ UPGraph ∧ F ∈ U ∧ P ∈ Z → F Walks ⁡ G P ↔ F ∈ Word dom ⁡ I ∧ P : 0 … F ⟶ V ∧ ∀ k ∈ 0 ..^ F I ⁡ F ⁡ k = P ⁡ k P ⁡ k + 1