This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lfgrn1cycl

Description: In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017) (Revised by AV, 2-Feb-2021)

Ref Expression
Hypotheses lfgrn1cycl.v 
|- V = ( Vtx ` G )
lfgrn1cycl.i 
|- I = ( iEdg ` G )
Assertion lfgrn1cycl 
|- ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( F ( Cycles ` G ) P -> ( # ` F ) =/= 1 ) )

Proof

Step Hyp Ref Expression
1 lfgrn1cycl.v 
 |-  V = ( Vtx ` G )
2 lfgrn1cycl.i 
 |-  I = ( iEdg ` G )
3 cyclprop 
 |-  ( F ( Cycles ` G ) P -> ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
4 cycliswlk 
 |-  ( F ( Cycles ` G ) P -> F ( Walks ` G ) P )
5 2 1 lfgrwlknloop 
 |-  ( ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
6 1nn 
 |-  1 e. NN
7 eleq1 
 |-  ( ( # ` F ) = 1 -> ( ( # ` F ) e. NN <-> 1 e. NN ) )
8 6 7 mpbiri 
 |-  ( ( # ` F ) = 1 -> ( # ` F ) e. NN )
9 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) <-> ( # ` F ) e. NN )
10 8 9 sylibr 
 |-  ( ( # ` F ) = 1 -> 0 e. ( 0 ..^ ( # ` F ) ) )
11 fveq2 
 |-  ( k = 0 -> ( P ` k ) = ( P ` 0 ) )
12 fv0p1e1 
 |-  ( k = 0 -> ( P ` ( k + 1 ) ) = ( P ` 1 ) )
13 11 12 neeq12d 
 |-  ( k = 0 -> ( ( P ` k ) =/= ( P ` ( k + 1 ) ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
14 13 rspcv 
 |-  ( 0 e. ( 0 ..^ ( # ` F ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( P ` 0 ) =/= ( P ` 1 ) ) )
15 10 14 syl 
 |-  ( ( # ` F ) = 1 -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( P ` 0 ) =/= ( P ` 1 ) ) )
16 15 impcom 
 |-  ( ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ ( # ` F ) = 1 ) -> ( P ` 0 ) =/= ( P ` 1 ) )
17 fveq2 
 |-  ( ( # ` F ) = 1 -> ( P ` ( # ` F ) ) = ( P ` 1 ) )
18 17 neeq2d 
 |-  ( ( # ` F ) = 1 -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
19 18 adantl 
 |-  ( ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ ( # ` F ) = 1 ) -> ( ( P ` 0 ) =/= ( P ` ( # ` F ) ) <-> ( P ` 0 ) =/= ( P ` 1 ) ) )
20 16 19 mpbird 
 |-  ( ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ ( # ` F ) = 1 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
21 20 ex 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( ( # ` F ) = 1 -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) )
22 21 necon2d 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( # ` F ) =/= 1 ) )
23 5 22 syl 
 |-  ( ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } /\ F ( Walks ` G ) P ) -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( # ` F ) =/= 1 ) )
24 23 ex 
 |-  ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( F ( Walks ` G ) P -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( # ` F ) =/= 1 ) ) )
25 24 com13 
 |-  ( ( P ` 0 ) = ( P ` ( # ` F ) ) -> ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( # ` F ) =/= 1 ) ) )
26 25 adantl 
 |-  ( ( F ( Paths ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( # ` F ) =/= 1 ) ) )
27 3 4 26 sylc 
 |-  ( F ( Cycles ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( # ` F ) =/= 1 ) )
28 27 com12 
 |-  ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( F ( Cycles ` G ) P -> ( # ` F ) =/= 1 ) )