isclwlk

Description: A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018) (Revised by AV, 16-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	isclwlk	$⊢ F ClWalks (G) P \leftrightarrow (F Walks (G) P \land P (0) = P (\|F\|))$

Proof

Step	Hyp	Ref	Expression
1		clwlks	$⊢ ClWalks (G) = \{⟨f, p⟩ \| (f Walks (G) p \land p (0) = p (\|f\|))\}$
2		fveq1	$⊢ p = P \to p (0) = P (0)$
3	2	adantl	$⊢ (f = F \land p = P) \to p (0) = P (0)$
4		simpr	$⊢ (f = F \land p = P) \to p = P$
5		fveq2	$⊢ f = F \to \|f\| = \|F\|$
6	5	adantr	$⊢ (f = F \land p = P) \to \|f\| = \|F\|$
7	4 6	fveq12d	$⊢ (f = F \land p = P) \to p (\|f\|) = P (\|F\|)$
8	3 7	eqeq12d	$⊢ (f = F \land p = P) \to (p (0) = p (\|f\|) \leftrightarrow P (0) = P (\|F\|))$
9		relwlk	$⊢ Rel Walks (G)$
10	1 8 9	brfvopabrbr	$⊢ F ClWalks (G) P \leftrightarrow (F Walks (G) P \land P (0) = P (\|F\|))$

Metamath Proof Explorer

Theorem isclwlk

Proof