Metamath Proof Explorer

Theorem lfgrwlkprop

Description: Two adjacent vertices in a walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021)

Ref Expression
Hypothesis lfgrwlkprop.i 
|- I = ( iEdg ` G )
Assertion lfgrwlkprop 
|- ( ( F ( Walks ` G ) P /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i 
 |-  I = ( iEdg ` G )
2 wlkv 
 |-  ( F ( Walks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
3 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
4 3 1 iswlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
5 2 4 syl 
 |-  ( F ( Walks ` G ) P -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
6 ifptru 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> ( I ` ( F ` k ) ) = { ( P ` k ) } ) )
7 6 adantr 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> ( I ` ( F ` k ) ) = { ( P ` k ) } ) )
8 simplr 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } )
9 wrdsymbcl 
 |-  ( ( F e. Word dom I /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` k ) e. dom I )
10 9 ad4ant14 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` k ) e. dom I )
11 8 10 ffvelcdmd 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( I ` ( F ` k ) ) e. { x e. ~P V | 2 <_ ( # ` x ) } )
12 fveq2 
 |-  ( x = ( I ` ( F ` k ) ) -> ( # ` x ) = ( # ` ( I ` ( F ` k ) ) ) )
13 12 breq2d 
 |-  ( x = ( I ` ( F ` k ) ) -> ( 2 <_ ( # ` x ) <-> 2 <_ ( # ` ( I ` ( F ` k ) ) ) ) )
14 13 elrab 
 |-  ( ( I ` ( F ` k ) ) e. { x e. ~P V | 2 <_ ( # ` x ) } <-> ( ( I ` ( F ` k ) ) e. ~P V /\ 2 <_ ( # ` ( I ` ( F ` k ) ) ) ) )
15 fveq2 
 |-  ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( # ` ( I ` ( F ` k ) ) ) = ( # ` { ( P ` k ) } ) )
16 15 breq2d 
 |-  ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( 2 <_ ( # ` ( I ` ( F ` k ) ) ) <-> 2 <_ ( # ` { ( P ` k ) } ) ) )
17 fvex 
 |-  ( P ` k ) e. _V
18 hashsng 
 |-  ( ( P ` k ) e. _V -> ( # ` { ( P ` k ) } ) = 1 )
19 17 18 ax-mp 
 |-  ( # ` { ( P ` k ) } ) = 1
20 19 breq2i 
 |-  ( 2 <_ ( # ` { ( P ` k ) } ) <-> 2 <_ 1 )
21 1lt2 
 |-  1 < 2
22 1re 
 |-  1 e. RR
23 2re 
 |-  2 e. RR
24 22 23 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
25 pm2.21 
 |-  ( -. 2 <_ 1 -> ( 2 <_ 1 -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
26 24 25 sylbi 
 |-  ( 1 < 2 -> ( 2 <_ 1 -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
27 21 26 ax-mp 
 |-  ( 2 <_ 1 -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
28 20 27 sylbi 
 |-  ( 2 <_ ( # ` { ( P ` k ) } ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
29 16 28 biimtrdi 
 |-  ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( 2 <_ ( # ` ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
30 29 com12 
 |-  ( 2 <_ ( # ` ( I ` ( F ` k ) ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
31 30 adantl 
 |-  ( ( ( I ` ( F ` k ) ) e. ~P V /\ 2 <_ ( # ` ( I ` ( F ` k ) ) ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
32 31 a1i 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( I ` ( F ` k ) ) e. ~P V /\ 2 <_ ( # ` ( I ` ( F ` k ) ) ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
33 14 32 biimtrid 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( I ` ( F ` k ) ) e. { x e. ~P V | 2 <_ ( # ` x ) } -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
34 11 33 mpd 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
35 34 adantl 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) ) -> ( ( I ` ( F ` k ) ) = { ( P ` k ) } -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
36 7 35 sylbid 
 |-  ( ( ( P ` k ) = ( P ` ( k + 1 ) ) /\ ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
37 36 ex 
 |-  ( ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
38 neqne 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) )
39 38 2a1d 
 |-  ( -. ( P ` k ) = ( P ` ( k + 1 ) ) -> ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
40 37 39 pm2.61i 
 |-  ( ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
41 40 ralimdva 
 |-  ( ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
42 41 ex 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
43 42 com23 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
44 43 3impia 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
45 5 44 biimtrdi 
 |-  ( F ( Walks ` G ) P -> ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) ) )
46 45 pm2.43i 
 |-  ( F ( Walks ` G ) P -> ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
47 46 imp 
 |-  ( ( F ( Walks ` G ) P /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )