Metamath Proof Explorer

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}\mathrm{Circuits}\left({G}\right){P}↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$

Proof

Step Hyp Ref Expression
1 crcts ${⊢}\mathrm{Circuits}\left({G}\right)=\left\{⟨{f},{p}⟩|\left({f}\mathrm{Trails}\left({G}\right){p}\wedge {p}\left(0\right)={p}\left(\left|{f}\right|\right)\right)\right\}$
2 fveq1 ${⊢}{p}={P}\to {p}\left(0\right)={P}\left(0\right)$
3 2 adantl ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(0\right)={P}\left(0\right)$
4 simpr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}={P}$
5 fveq2 ${⊢}{f}={F}\to \left|{f}\right|=\left|{F}\right|$
6 5 adantr ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left|{f}\right|=\left|{F}\right|$
7 4 6 fveq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to {p}\left(\left|{f}\right|\right)={P}\left(\left|{F}\right|\right)$
8 3 7 eqeq12d ${⊢}\left({f}={F}\wedge {p}={P}\right)\to \left({p}\left(0\right)={p}\left(\left|{f}\right|\right)↔{P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
9 reltrls ${⊢}\mathrm{Rel}\mathrm{Trails}\left({G}\right)$
10 1 8 9 brfvopabrbr ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}↔\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$