Metamath Proof Explorer

Theorem cyclnspth

Description: A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017) (Revised by AV, 31-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

Ref Expression
Assertion cyclnspth 
|- ( F =/= (/) -> ( F ( Cycles ` G ) P -> -. F ( SPaths ` G ) P ) )

Proof

Step Hyp Ref Expression
1 iscycl 
 |-  ( F ( Cycles ` G ) P <-> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
2 relpths 
 |-  Rel ( Paths ` G )
3 2 brrelex1i 
 |-  ( F ( Paths ` G ) P -> F e. _V )
4 hasheq0 
 |-  ( F e. _V -> ( ( # ` F ) = 0 <-> F = (/) ) )
5 4 necon3bid 
 |-  ( F e. _V -> ( ( # ` F ) =/= 0 <-> F =/= (/) ) )
6 5 bicomd 
 |-  ( F e. _V -> ( F =/= (/) <-> ( # ` F ) =/= 0 ) )
7 3 6 syl 
 |-  ( F ( Paths ` G ) P -> ( F =/= (/) <-> ( # ` F ) =/= 0 ) )
8 7 biimpa 
 |-  ( ( F ( Paths ` G ) P /\ F =/= (/) ) -> ( # ` F ) =/= 0 )
9 spthdep 
 |-  ( ( F ( SPaths ` G ) P /\ ( # ` F ) =/= 0 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
10 9 neneqd 
 |-  ( ( F ( SPaths ` G ) P /\ ( # ` F ) =/= 0 ) -> -. ( P ` 0 ) = ( P ` ( # ` F ) ) )
11 10 expcom 
 |-  ( ( # ` F ) =/= 0 -> ( F ( SPaths ` G ) P -> -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
12 8 11 syl 
 |-  ( ( F ( Paths ` G ) P /\ F =/= (/) ) -> ( F ( SPaths ` G ) P -> -. ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
13 12 con2d 
 |-  ( ( F ( Paths ` G ) P /\ F =/= (/) ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> -. F ( SPaths ` G ) P ) )
14 13 impancom 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( F =/= (/) -> -. F ( SPaths ` G ) P ) )
15 1 14 sylbi 
 |-  ( F ( Cycles ` G ) P -> ( F =/= (/) -> -. F ( SPaths ` G ) P ) )
16 15 com12 
 |-  ( F =/= (/) -> ( F ( Cycles ` G ) P -> -. F ( SPaths ` G ) P ) )