# Metamath Proof Explorer

## Theorem usgr2trlncrct

Description: In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021)

Ref Expression
Assertion usgr2trlncrct ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\to \left({F}\mathrm{Trails}\left({G}\right){P}\to ¬{F}\mathrm{Circuits}\left({G}\right){P}\right)$

### Proof

Step Hyp Ref Expression
1 usgr2trlncl ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\to \left({F}\mathrm{Trails}\left({G}\right){P}\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
2 1 imp ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to {P}\left(0\right)\ne {P}\left(2\right)$
3 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)$
4 fveq2 ${⊢}\left|{F}\right|=2\to {P}\left(\left|{F}\right|\right)={P}\left(2\right)$
5 4 eqeq2d ${⊢}\left|{F}\right|=2\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)↔{P}\left(0\right)={P}\left(2\right)\right)$
6 5 biimpcd ${⊢}{P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left(\left|{F}\right|=2\to {P}\left(0\right)={P}\left(2\right)\right)$
7 3 6 simpl2im ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to \left(\left|{F}\right|=2\to {P}\left(0\right)={P}\left(2\right)\right)$
8 7 com12 ${⊢}\left|{F}\right|=2\to \left({F}\mathrm{Circuits}\left({G}\right){P}\to {P}\left(0\right)={P}\left(2\right)\right)$
9 8 ad2antlr ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to \left({F}\mathrm{Circuits}\left({G}\right){P}\to {P}\left(0\right)={P}\left(2\right)\right)$
10 9 necon3ad ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to \left({P}\left(0\right)\ne {P}\left(2\right)\to ¬{F}\mathrm{Circuits}\left({G}\right){P}\right)$
11 2 10 mpd ${⊢}\left(\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\wedge {F}\mathrm{Trails}\left({G}\right){P}\right)\to ¬{F}\mathrm{Circuits}\left({G}\right){P}$
12 11 ex ${⊢}\left({G}\in \mathrm{USGraph}\wedge \left|{F}\right|=2\right)\to \left({F}\mathrm{Trails}\left({G}\right){P}\to ¬{F}\mathrm{Circuits}\left({G}\right){P}\right)$