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 ) )