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	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ¬ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		usgr2trlncl	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) )
2	1	imp	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) )
3		crctprop	⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) )
4		fveq2	⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) = ( 𝑃 ‘ 2 ) )
5	4	eqeq2d	⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ↔ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ) )
6	5	biimpcd	⊢ ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ) )
7	3 6	simpl2im	⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ) )
8	7	com12	⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ) )
9	8	ad2antlr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ 2 ) ) )
10	9	necon3ad	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) → ¬ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) )
11	2 10	mpd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) ∧ 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ) → ¬ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 )
12	11	ex	⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 → ¬ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) )