Theorem 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 <-> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		crcts	|- ( Circuits ` G ) = { <. f , p >. | ( f ( Trails ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) }
2		fveq1	|- ( p = P -> ( p ` 0 ) = ( P ` 0 ) )
3	2	adantl	|- ( ( f = F /\ p = P ) -> ( p ` 0 ) = ( P ` 0 ) )
4		simpr	|- ( ( f = F /\ p = P ) -> p = P )
5		fveq2	|- ( f = F -> ( # ` f ) = ( # ` F ) )
6	5	adantr	|- ( ( f = F /\ p = P ) -> ( # ` f ) = ( # ` F ) )
7	4 6	fveq12d	|- ( ( f = F /\ p = P ) -> ( p ` ( # ` f ) ) = ( P ` ( # ` F ) ) )
8	3 7	eqeq12d	|- ( ( f = F /\ p = P ) -> ( ( p ` 0 ) = ( p ` ( # ` f ) ) <-> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
9		reltrls	|- Rel ( Trails ` G )
10	1 8 9	brfvopabrbr	|- ( F ( Circuits ` G ) P <-> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )