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

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 Circuits ⁡ G P → F ClWalks ⁡ G P

Proof

Step Hyp Ref Expression
1 crctprop ⊢ F Circuits ⁡ G P → F Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ F
2 trliswlk ⊢ F Trails ⁡ G P → F Walks ⁡ G P
3 isclwlk ⊢ F ClWalks ⁡ G P ↔ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F
4 3 biimpri ⊢ F Walks ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F ClWalks ⁡ G P
5 2 4 sylan ⊢ F Trails ⁡ G P ∧ P ⁡ 0 = P ⁡ F → F ClWalks ⁡ G P
6 1 5 syl ⊢ F Circuits ⁡ G P → F ClWalks ⁡ G P