Metamath Proof Explorer

Theorem crctisclwlk

Description: A circuit is a closed walk. (Contributed by AV, 17-Feb-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion crctisclwlk ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{ClWalks}\left({G}\right){P}$

Proof

Step Hyp Ref Expression
1 crctprop ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to \left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
2 trliswlk ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to {F}\mathrm{Walks}\left({G}\right){P}$
3 isclwlk ${⊢}{F}\mathrm{ClWalks}\left({G}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
4 3 biimpri ${⊢}\left({F}\mathrm{Walks}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to {F}\mathrm{ClWalks}\left({G}\right){P}$
5 2 4 sylan ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to {F}\mathrm{ClWalks}\left({G}\right){P}$
6 1 5 syl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to {F}\mathrm{ClWalks}\left({G}\right){P}$