iscrct

Description: Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Revised by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	iscrct	$⊢ F Circuits (G) P \leftrightarrow (F Trails (G) P \land P (0) = P (\|F\|))$

Proof

Step	Hyp	Ref	Expression
1		crcts	$⊢ Circuits (G) = \{⟨f, p⟩ \| (f Trails (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		reltrls	$⊢ Rel Trails (G)$
10	1 8 9	brfvopabrbr	$⊢ F Circuits (G) P \leftrightarrow (F Trails (G) P \land P (0) = P (\|F\|))$

Metamath Proof Explorer

Theorem iscrct

Proof