Metamath Proof Explorer

Theorem spthdep

Description: A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
2 trliswlk 
 |-  ( F ( Trails ` G ) P -> F ( Walks ` G ) P )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
5 2 4 syl 
 |-  ( F ( Trails ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
6 5 anim1i 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) )
7 df-f1 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) )
8 6 7 sylibr 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) )
9 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
10 nn0fz0 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
11 10 biimpi 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
12 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
13 11 12 jca 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
14 2 9 13 3syl 
 |-  ( F ( Trails ` G ) P -> ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
15 14 adantr 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
16 8 15 jca 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) ) )
17 eqcom 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` ( # ` F ) ) = ( P ` 0 ) )
18 f1veqaeq 
 |-  ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) ) -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( # ` F ) = 0 ) )
19 17 18 syl5bi 
 |-  ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( # ` F ) = 0 ) )
20 16 19 syl 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( # ` F ) = 0 ) )
21 20 necon3d 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( ( # ` F ) =/= 0 -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
22 1 21 sylbi 
 |-  ( F ( SPaths ` G ) P -> ( ( # ` F ) =/= 0 -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
23 22 imp 
 |-  ( ( F ( SPaths ` G ) P /\ ( # ` F ) =/= 0 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )