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

Metamath Proof Explorer

Theorem cycliscrct

Description: A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

		Ref	Expression
	Assertion	cycliscrct	$⊢ F Cycles (G) P \to F Circuits (G) P$

Proof

Step	Hyp	Ref	Expression
1		pthistrl	$⊢ F Paths (G) P \to F Trails (G) P$
2	1	anim1i	$⊢ (F Paths (G) P \land P (0) = P (\|F\|)) \to (F Trails (G) P \land P (0) = P (\|F\|))$
3		iscycl	$⊢ F Cycles (G) P \leftrightarrow (F Paths (G) P \land P (0) = P (\|F\|))$
4		iscrct	$⊢ F Circuits (G) P \leftrightarrow (F Trails (G) P \land P (0) = P (\|F\|))$
5	2 3 4	3imtr4i	$⊢ F Cycles (G) P \to F Circuits (G) P$