Metamath Proof Explorer

Theorem spthonepeq

Description: The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018) (Revised by AV, 18-Jan-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion spthonepeq 
|- ( F ( A ( SPathsOn ` G ) B ) P -> ( A = B <-> ( # ` F ) = 0 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 1 spthonprop 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) )
3 1 istrlson 
 |-  ( ( ( A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
4 3 3adantl1 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( TrailsOn ` G ) B ) P <-> ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) ) )
5 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
6 5 a1i 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) ) )
7 4 6 anbi12d 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) <-> ( ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) /\ ( F ( Trails ` G ) P /\ Fun `' P ) ) ) )
8 1 wlkonprop 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
9 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
10 1 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
11 df-f1 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) <-> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) )
12 eqeq2 
 |-  ( A = B -> ( ( P ` 0 ) = A <-> ( P ` 0 ) = B ) )
13 eqtr3 
 |-  ( ( ( P ` ( # ` F ) ) = B /\ ( P ` 0 ) = B ) -> ( P ` ( # ` F ) ) = ( P ` 0 ) )
14 elnn0uz 
 |-  ( ( # ` F ) e. NN0 <-> ( # ` F ) e. ( ZZ>= ` 0 ) )
15 eluzfz2 
 |-  ( ( # ` F ) e. ( ZZ>= ` 0 ) -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
16 14 15 sylbi 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. ( 0 ... ( # ` F ) ) )
17 0elfz 
 |-  ( ( # ` F ) e. NN0 -> 0 e. ( 0 ... ( # ` F ) ) )
18 16 17 jca 
 |-  ( ( # ` F ) e. NN0 -> ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) )
19 f1veqaeq 
 |-  ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( ( # ` F ) e. ( 0 ... ( # ` F ) ) /\ 0 e. ( 0 ... ( # ` F ) ) ) ) -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( # ` F ) = 0 ) )
20 18 19 sylan2 
 |-  ( ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) /\ ( # ` F ) e. NN0 ) -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( # ` F ) = 0 ) )
21 20 ex 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( ( # ` F ) e. NN0 -> ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( # ` F ) = 0 ) ) )
22 21 com13 
 |-  ( ( P ` ( # ` F ) ) = ( P ` 0 ) -> ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( # ` F ) = 0 ) ) )
23 13 22 syl 
 |-  ( ( ( P ` ( # ` F ) ) = B /\ ( P ` 0 ) = B ) -> ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( # ` F ) = 0 ) ) )
24 23 expcom 
 |-  ( ( P ` 0 ) = B -> ( ( P ` ( # ` F ) ) = B -> ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( # ` F ) = 0 ) ) ) )
25 12 24 syl6bi 
 |-  ( A = B -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( # ` F ) = 0 ) ) ) ) )
26 25 com15 
 |-  ( P : ( 0 ... ( # ` F ) ) -1-1-> ( Vtx ` G ) -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( ( # ` F ) e. NN0 -> ( A = B -> ( # ` F ) = 0 ) ) ) ) )
27 11 26 sylbir 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ Fun `' P ) -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( ( # ` F ) e. NN0 -> ( A = B -> ( # ` F ) = 0 ) ) ) ) )
28 27 expcom 
 |-  ( Fun `' P -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( ( # ` F ) e. NN0 -> ( A = B -> ( # ` F ) = 0 ) ) ) ) ) )
29 28 com15 
 |-  ( ( # ` F ) e. NN0 -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( Fun `' P -> ( A = B -> ( # ` F ) = 0 ) ) ) ) ) )
30 9 10 29 sylc 
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) = A -> ( ( P ` ( # ` F ) ) = B -> ( Fun `' P -> ( A = B -> ( # ` F ) = 0 ) ) ) ) )
31 30 3imp1 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ Fun `' P ) -> ( A = B -> ( # ` F ) = 0 ) )
32 fveqeq2 
 |-  ( ( # ` F ) = 0 -> ( ( P ` ( # ` F ) ) = B <-> ( P ` 0 ) = B ) )
33 32 anbi2d 
 |-  ( ( # ` F ) = 0 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) <-> ( ( P ` 0 ) = A /\ ( P ` 0 ) = B ) ) )
34 eqtr2 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 0 ) = B ) -> A = B )
35 33 34 syl6bi 
 |-  ( ( # ` F ) = 0 -> ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> A = B ) )
36 35 com12 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` F ) = 0 -> A = B ) )
37 36 3adant1 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( ( # ` F ) = 0 -> A = B ) )
38 37 adantr 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ Fun `' P ) -> ( ( # ` F ) = 0 -> A = B ) )
39 31 38 impbid 
 |-  ( ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) /\ Fun `' P ) -> ( A = B <-> ( # ` F ) = 0 ) )
40 39 ex 
 |-  ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) -> ( Fun `' P -> ( A = B <-> ( # ` F ) = 0 ) ) )
41 40 3ad2ant3 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> ( Fun `' P -> ( A = B <-> ( # ` F ) = 0 ) ) )
42 8 41 syl 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( Fun `' P -> ( A = B <-> ( # ` F ) = 0 ) ) )
43 42 adantld 
 |-  ( F ( A ( WalksOn ` G ) B ) P -> ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( A = B <-> ( # ` F ) = 0 ) ) )
44 43 adantr 
 |-  ( ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) -> ( ( F ( Trails ` G ) P /\ Fun `' P ) -> ( A = B <-> ( # ` F ) = 0 ) ) )
45 44 imp 
 |-  ( ( ( F ( A ( WalksOn ` G ) B ) P /\ F ( Trails ` G ) P ) /\ ( F ( Trails ` G ) P /\ Fun `' P ) ) -> ( A = B <-> ( # ` F ) = 0 ) )
46 7 45 syl6bi 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) ) -> ( ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) -> ( A = B <-> ( # ` F ) = 0 ) ) )
47 46 3impia 
 |-  ( ( ( G e. _V /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( TrailsOn ` G ) B ) P /\ F ( SPaths ` G ) P ) ) -> ( A = B <-> ( # ` F ) = 0 ) )
48 2 47 syl 
 |-  ( F ( A ( SPathsOn ` G ) B ) P -> ( A = B <-> ( # ` F ) = 0 ) )