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 \in V \land B \in V) \land (F \in U \land P \in Z)) \to (F (A WalksOn (G) B) P \leftrightarrow (F Walks (G) P \land P (0) = A \land P (\|F\|) = B))$

Proof

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