# 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}=\mathrm{Vtx}\left({G}\right)$
Assertion iswlkon ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {U}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 wlkson.v ${⊢}{V}=\mathrm{Vtx}\left({G}\right)$
2 1 wlkson ${⊢}\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\mathrm{WalksOn}\left({G}\right){B}=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Walks}\left({G}\right){p}\wedge {p}\left(0\right)={A}\wedge {p}\left(\left|{f}\right|\right)={B}\right)\right\}$
3 fveq1 ${⊢}{p}={P}\to {p}\left(0\right)={P}\left(0\right)$
4 3 adantl ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(0\right)={P}\left(0\right)$
5 4 eqeq1d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({p}\left(0\right)={A}↔{P}\left(0\right)={A}\right)$
6 simpr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}={P}$
7 fveq2 ${⊢}{f}={F}\to \left|{f}\right|=\left|{F}\right|$
8 7 adantr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left|{f}\right|=\left|{F}\right|$
9 6 8 fveq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(\left|{f}\right|\right)={P}\left(\left|{F}\right|\right)$
10 9 eqeq1d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({p}\left(\left|{f}\right|\right)={B}↔{P}\left(\left|{F}\right|\right)={B}\right)$
11 2 5 10 2rbropap ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge {F}\in {U}\wedge {P}\in {Z}\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$
12 11 3expb ${⊢}\left(\left({A}\in {V}\wedge {B}\in {V}\right)\wedge \left({F}\in {U}\wedge {P}\in {Z}\right)\right)\to \left({F}\left({A}\mathrm{WalksOn}\left({G}\right){B}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={A}\wedge {P}\left(\left|{F}\right|\right)={B}\right)\right)$