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

Metamath Proof Explorer

Theorem iswlkon

Description: Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017) (Revised by AV, 31-Dec-2020) (Revised by AV, 22-Mar-2021)

Ref Expression
Hypothesis wlkson.v ⊢ V = Vtx ⁡ G
Assertion iswlkon ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B

Proof

Step Hyp Ref Expression
1 wlkson.v ⊢ V = Vtx ⁡ G
2 1 wlkson ⊢ A ∈ V ∧ B ∈ V → A WalksOn ⁡ G B = f p | f Walks ⁡ G p ∧ p ⁡ 0 = A ∧ p ⁡ f = B
3 fveq1 ⊢ p = P → p ⁡ 0 = P ⁡ 0
4 3 adantl ⊢ f = F ∧ p = P → p ⁡ 0 = P ⁡ 0
5 4 eqeq1d ⊢ f = F ∧ p = P → p ⁡ 0 = A ↔ P ⁡ 0 = A
6 simpr ⊢ f = F ∧ p = P → p = P
7 fveq2 ⊢ f = F → f = F
8 7 adantr ⊢ f = F ∧ p = P → f = F
9 6 8 fveq12d ⊢ f = F ∧ p = P → p ⁡ f = P ⁡ F
10 9 eqeq1d ⊢ f = F ∧ p = P → p ⁡ f = B ↔ P ⁡ F = B
11 2 5 10 2rbropap ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B
12 11 3expb ⊢ A ∈ V ∧ B ∈ V ∧ F ∈ U ∧ P ∈ Z → F A WalksOn ⁡ G B P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = A ∧ P ⁡ F = B