Metamath Proof Explorer

Theorem spthcycl

Description: A walk is a trivial path if and only if it is both a simple path and a cycle. (Contributed by BTernaryTau, 8-Oct-2023)

Ref Expression
Assertion spthcycl 
|- ( ( F ( Paths ` G ) P /\ F = (/) ) <-> ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) )

Proof

Step Hyp Ref Expression
1 pthistrl 
 |-  ( F ( Paths ` G ) P -> F ( Trails ` G ) P )
2 pthiswlk 
 |-  ( F ( Paths ` 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 4 ffund 
 |-  ( F ( Walks ` G ) P -> Fun P )
6 wlklenvp1 
 |-  ( F ( Walks ` G ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
7 6 adantr 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> ( # ` P ) = ( ( # ` F ) + 1 ) )
8 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
9 8 simp2d 
 |-  ( F ( Walks ` G ) P -> F e. _V )
10 hasheq0 
 |-  ( F e. _V -> ( ( # ` F ) = 0 <-> F = (/) ) )
11 10 biimpar 
 |-  ( ( F e. _V /\ F = (/) ) -> ( # ` F ) = 0 )
12 9 11 sylan 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> ( # ` F ) = 0 )
13 oveq1 
 |-  ( ( # ` F ) = 0 -> ( ( # ` F ) + 1 ) = ( 0 + 1 ) )
14 0p1e1 
 |-  ( 0 + 1 ) = 1
15 13 14 eqtrdi 
 |-  ( ( # ` F ) = 0 -> ( ( # ` F ) + 1 ) = 1 )
16 12 15 syl 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> ( ( # ` F ) + 1 ) = 1 )
17 7 16 eqtrd 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> ( # ` P ) = 1 )
18 8 simp3d 
 |-  ( F ( Walks ` G ) P -> P e. _V )
19 hashen1 
 |-  ( P e. _V -> ( ( # ` P ) = 1 <-> P ~~ 1o ) )
20 18 19 syl 
 |-  ( F ( Walks ` G ) P -> ( ( # ` P ) = 1 <-> P ~~ 1o ) )
21 20 biimpa 
 |-  ( ( F ( Walks ` G ) P /\ ( # ` P ) = 1 ) -> P ~~ 1o )
22 17 21 syldan 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> P ~~ 1o )
23 funen1cnv 
 |-  ( ( Fun P /\ P ~~ 1o ) -> Fun `' P )
24 5 22 23 syl2an2r 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> Fun `' P )
25 2 24 sylan 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> Fun `' P )
26 isspth 
 |-  ( F ( SPaths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' P ) )
27 26 biimpri 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' P ) -> F ( SPaths ` G ) P )
28 1 25 27 syl2an2r 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> F ( SPaths ` G ) P )
29 fveq2 
 |-  ( 0 = ( # ` F ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
30 29 eqcoms 
 |-  ( ( # ` F ) = 0 -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
31 12 30 syl 
 |-  ( ( F ( Walks ` G ) P /\ F = (/) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
32 2 31 sylan 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> ( P ` 0 ) = ( P ` ( # ` F ) ) )
33 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
34 33 biimpri 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> F ( Cycles ` G ) P )
35 32 34 syldan 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> F ( Cycles ` G ) P )
36 28 35 jca 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) -> ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) )
37 spthispth 
 |-  ( F ( SPaths ` G ) P -> F ( Paths ` G ) P )
38 37 adantr 
 |-  ( ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) -> F ( Paths ` G ) P )
39 notnot 
 |-  ( F ( SPaths ` G ) P -> -. -. F ( SPaths ` G ) P )
40 cyclnspth 
 |-  ( F =/= (/) -> ( F ( Cycles ` G ) P -> -. F ( SPaths ` G ) P ) )
41 40 com12 
 |-  ( F ( Cycles ` G ) P -> ( F =/= (/) -> -. F ( SPaths ` G ) P ) )
42 41 con3dimp 
 |-  ( ( F ( Cycles ` G ) P /\ -. -. F ( SPaths ` G ) P ) -> -. F =/= (/) )
43 nne 
 |-  ( -. F =/= (/) <-> F = (/) )
44 42 43 sylib 
 |-  ( ( F ( Cycles ` G ) P /\ -. -. F ( SPaths ` G ) P ) -> F = (/) )
45 39 44 sylan2 
 |-  ( ( F ( Cycles ` G ) P /\ F ( SPaths ` G ) P ) -> F = (/) )
46 45 ancoms 
 |-  ( ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) -> F = (/) )
47 38 46 jca 
 |-  ( ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) -> ( F ( Paths ` G ) P /\ F = (/) ) )
48 36 47 impbii 
 |-  ( ( F ( Paths ` G ) P /\ F = (/) ) <-> ( F ( SPaths ` G ) P /\ F ( Cycles ` G ) P ) )