Metamath Proof Explorer

Theorem pthdepisspth

Description: A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017) (Revised by AV, 12-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion pthdepisspth 
|- ( ( F ( Paths ` G ) P /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> F ( SPaths ` G ) P )

Proof

Step Hyp Ref Expression
1 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
2 simplll 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> F ( Trails ` G ) P )
3 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
4 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
5 3 4 syl 
 |-  ( F ( Trails ` G ) P -> ( # ` F ) e. NN0 )
6 5 ad3antrrr 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( # ` F ) e. NN0 )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
9 3 8 syl 
 |-  ( F ( Trails ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
10 9 ad3antrrr 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
11 simpllr 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
12 simpr 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
13 10 11 12 3jca 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
14 simplr 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) )
15 injresinj 
 |-  ( ( # ` F ) e. NN0 -> ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> Fun `' P ) ) )
16 6 13 14 15 syl3c 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> Fun `' P )
17 2 16 jca 
 |-  ( ( ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( F ( Trails ` G ) P /\ Fun `' P ) )
18 17 ex3 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) -> ( F ( Trails ` G ) P /\ Fun `' P ) ) )
19 1 18 sylbi 
 |-  ( F ( Paths ` G ) P -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) -> ( F ( Trails ` G ) P /\ Fun `' P ) ) )
20 19 imp 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> ( F ( Trails ` G ) P /\ Fun `' P ) )
21 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
22 20 21 sylibr 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> F ( SPaths ` G ) P )