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 
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> -. F ( Circuits ` G ) P ) )

Proof

Step Hyp Ref Expression
1 usgr2trlncl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> ( P ` 0 ) =/= ( P ` 2 ) ) )
2 1 imp 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( P ` 0 ) =/= ( P ` 2 ) )
3 crctprop 
 |-  ( F ( Circuits ` G ) P -> ( F ( Trails ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 fveq2 
 |-  ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = ( P ` 2 ) )
5 4 eqeq2d 
 |-  ( ( # ` F ) = 2 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 2 ) ) )
6 5 biimpcd 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( ( # ` F ) = 2 -> ( P ` 0 ) = ( P ` 2 ) ) )
7 3 6 simpl2im 
 |-  ( F ( Circuits ` G ) P -> ( ( # ` F ) = 2 -> ( P ` 0 ) = ( P ` 2 ) ) )
8 7 com12 
 |-  ( ( # ` F ) = 2 -> ( F ( Circuits ` G ) P -> ( P ` 0 ) = ( P ` 2 ) ) )
9 8 ad2antlr 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( F ( Circuits ` G ) P -> ( P ` 0 ) = ( P ` 2 ) ) )
10 9 necon3ad 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> -. F ( Circuits ` G ) P ) )
11 2 10 mpd 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> -. F ( Circuits ` G ) P )
12 11 ex 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> -. F ( Circuits ` G ) P ) )