Metamath Proof Explorer

Theorem 2pthnloop

Description: A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon . (Contributed by AV, 6-Feb-2021)

Ref Expression
Hypothesis 2pthnloop.i 
|- I = ( iEdg ` G )
Assertion 2pthnloop 
|- ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 2pthnloop.i 
 |-  I = ( iEdg ` G )
2 pthiswlk 
 |-  ( F ( Paths ` G ) P -> F ( Walks ` G ) P )
3 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
4 2 3 syl 
 |-  ( F ( Paths ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
5 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
6 istrl 
 |-  ( F ( Trails ` G ) P <-> ( F ( Walks ` G ) P /\ Fun `' F ) )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 1 iswlkg 
 |-  ( G e. _V -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) ) )
9 8 anbi1d 
 |-  ( G e. _V -> ( ( F ( Walks ` G ) P /\ Fun `' F ) <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) /\ Fun `' F ) ) )
10 6 9 syl5bb 
 |-  ( G e. _V -> ( F ( Trails ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) /\ Fun `' F ) ) )
11 pthdadjvtx 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` i ) =/= ( P ` ( i + 1 ) ) )
12 11 ad5ant245 
 |-  ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( P ` i ) =/= ( P ` ( i + 1 ) ) )
13 12 neneqd 
 |-  ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> -. ( P ` i ) = ( P ` ( i + 1 ) ) )
14 ifpfal 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
15 14 adantl 
 |-  ( ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( P ` i ) = ( P ` ( i + 1 ) ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) <-> { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) )
16 fvexd 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( P ` i ) e. _V )
17 fvexd 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( P ` ( i + 1 ) ) e. _V )
18 neqne 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( P ` i ) =/= ( P ` ( i + 1 ) ) )
19 fvexd 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( I ` ( F ` i ) ) e. _V )
20 prsshashgt1 
 |-  ( ( ( ( P ` i ) e. _V /\ ( P ` ( i + 1 ) ) e. _V /\ ( P ` i ) =/= ( P ` ( i + 1 ) ) ) /\ ( I ` ( F ` i ) ) e. _V ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) -> 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
21 16 17 18 19 20 syl31anc 
 |-  ( -. ( P ` i ) = ( P ` ( i + 1 ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) -> 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
22 21 adantl 
 |-  ( ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( P ` i ) = ( P ` ( i + 1 ) ) ) -> ( { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) -> 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
23 15 22 sylbid 
 |-  ( ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) /\ -. ( P ` i ) = ( P ` ( i + 1 ) ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
24 13 23 mpdan 
 |-  ( ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) /\ i e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
25 24 ralimdva 
 |-  ( ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) /\ 1 < ( # ` F ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
26 25 ex 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) -> ( 1 < ( # ` F ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) )
27 26 com23 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ F ( Paths ` G ) P ) /\ ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) )
28 27 exp31 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( F ( Paths ` G ) P -> ( ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) )
29 28 com24 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) -> ( ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) )
30 29 3impia 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> ( ( ( Fun `' F /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) )
31 30 exp4c 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) -> ( Fun `' F -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) ) )
32 31 imp 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. i e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` i ) = ( P ` ( i + 1 ) ) , ( I ` ( F ` i ) ) = { ( P ` i ) } , { ( P ` i ) , ( P ` ( i + 1 ) ) } C_ ( I ` ( F ` i ) ) ) ) /\ Fun `' F ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) )
33 10 32 syl6bi 
 |-  ( G e. _V -> ( F ( Trails ` G ) P -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) ) )
34 33 com24 
 |-  ( G e. _V -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( F ( Trails ` G ) P -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) ) )
35 34 com14 
 |-  ( F ( Trails ` G ) P -> ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) -> ( ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) -> ( G e. _V -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) ) ) )
36 35 3imp 
 |-  ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( G e. _V -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) )
37 36 com12 
 |-  ( G e. _V -> ( ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) )
38 5 37 syl5bi 
 |-  ( G e. _V -> ( F ( Paths ` G ) P -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) )
39 38 3ad2ant1 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Paths ` G ) P -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) ) )
40 4 39 mpcom 
 |-  ( F ( Paths ` G ) P -> ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) ) )
41 40 pm2.43i 
 |-  ( F ( Paths ` G ) P -> ( 1 < ( # ` F ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) ) )
42 41 imp 
 |-  ( ( F ( Paths ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0 ..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) )