Metamath Proof Explorer

Theorem usgr2trlspth

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

Ref Expression
Assertion usgr2trlspth 
|- ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P <-> F ( SPaths ` 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 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
4 wlkonwlk 
 |-  ( F ( Walks ` G ) P -> F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P )
5 simpll 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> G e. USGraph )
6 simplr 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( # ` F ) = 2 )
7 fveq2 
 |-  ( ( # ` F ) = 2 -> ( P ` ( # ` F ) ) = ( P ` 2 ) )
8 7 eqcomd 
 |-  ( ( # ` F ) = 2 -> ( P ` 2 ) = ( P ` ( # ` F ) ) )
9 8 neeq2d 
 |-  ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` 2 ) <-> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
10 9 biimpd 
 |-  ( ( # ` F ) = 2 -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
11 10 adantl 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
12 11 imp 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
13 usgr2wlkspth 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P ) )
14 5 6 12 13 syl3anc 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P <-> F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P ) )
15 spthonisspth 
 |-  ( F ( ( P ` 0 ) ( SPathsOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P )
16 14 15 syl6bi 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ ( P ` 0 ) =/= ( P ` 2 ) ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P ) )
17 16 expcom 
 |-  ( ( P ` 0 ) =/= ( P ` 2 ) -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> F ( SPaths ` G ) P ) ) )
18 17 com13 
 |-  ( F ( ( P ` 0 ) ( WalksOn ` G ) ( P ` ( # ` F ) ) ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) ) )
19 3 4 18 3syl 
 |-  ( F ( Trails ` G ) P -> ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) ) )
20 19 impcom 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> ( ( P ` 0 ) =/= ( P ` 2 ) -> F ( SPaths ` G ) P ) )
21 2 20 mpd 
 |-  ( ( ( G e. USGraph /\ ( # ` F ) = 2 ) /\ F ( Trails ` G ) P ) -> F ( SPaths ` G ) P )
22 21 ex 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P -> F ( SPaths ` G ) P ) )
23 spthispth 
 |-  ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )
24 pthistrl 
 |-  ( F ( Paths ` G ) P -> F ( Trails ` G ) P )
25 23 24 syl 
 |-  ( F ( SPaths ` G ) P -> F ( Trails ` G ) P )
26 22 25 impbid1 
 |-  ( ( G e. USGraph /\ ( # ` F ) = 2 ) -> ( F ( Trails ` G ) P <-> F ( SPaths ` G ) P ) )