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	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Trails (G) P \to \neg F Circuits (G) P)$

Step	Hyp	Ref	Expression
1		usgr2trlncl	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Trails (G) P \to P (0) \neq P (2))$
2	1	imp	$⊢ ((G \in USGraph \land \|F\| = 2) \land F Trails (G) P) \to P (0) \neq P (2)$
3		crctprop	$⊢ F Circuits (G) P \to (F Trails (G) P \land P (0) = P (\|F\|))$
4		fveq2	$⊢ \|F\| = 2 \to P (\|F\|) = P (2)$
5	4	eqeq2d	$⊢ \|F\| = 2 \to (P (0) = P (\|F\|) \leftrightarrow P (0) = P (2))$
6	5	biimpcd	$⊢ P (0) = P (\|F\|) \to (\|F\| = 2 \to P (0) = P (2))$
7	3 6	simpl2im	$⊢ F Circuits (G) P \to (\|F\| = 2 \to P (0) = P (2))$
8	7	com12	$⊢ \|F\| = 2 \to (F Circuits (G) P \to P (0) = P (2))$
9	8	ad2antlr	$⊢ ((G \in USGraph \land \|F\| = 2) \land F Trails (G) P) \to (F Circuits (G) P \to P (0) = P (2))$
10	9	necon3ad	$⊢ ((G \in USGraph \land \|F\| = 2) \land F Trails (G) P) \to (P (0) \neq P (2) \to \neg F Circuits (G) P)$
11	2 10	mpd	$⊢ ((G \in USGraph \land \|F\| = 2) \land F Trails (G) P) \to \neg F Circuits (G) P$
12	11	ex	$⊢ (G \in USGraph \land \|F\| = 2) \to (F Trails (G) P \to \neg F Circuits (G) P)$

Metamath Proof Explorer