Metamath Proof Explorer

Theorem lfgriswlk

Description: Conditions for a pair of functions to be a walk in a loop-free graph. (Contributed by AV, 28-Jan-2021)

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

Proof

Step Hyp Ref Expression
1 lfgrwlkprop.i 
 |-  I = ( iEdg ` G )
2 lfgriswlk.v 
 |-  V = ( Vtx ` G )
3 1 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom I )
4 3 adantl 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> F e. Word dom I )
5 2 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
6 5 adantl 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> P : ( 0 ... ( # ` F ) ) --> V )
7 1 lfgrwlkprop 
 |-  ( ( F ( Walks ` G ) P /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
8 7 expcom 
 |-  ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
9 8 adantl 
 |-  ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) ) )
10 9 imp 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
11 1 wlkvtxeledg 
 |-  ( F ( Walks ` G ) P -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
12 11 adantl 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
13 r19.26 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) <-> ( A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
14 10 12 13 sylanbrc 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
15 4 6 14 3jca 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ F ( Walks ` G ) P ) -> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) )
16 simpr1 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) -> F e. Word dom I )
17 simpr2 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
18 df-ne 
 |-  ( ( P ` k ) =/= ( P ` ( k + 1 ) ) <-> -. ( P ` k ) = ( P ` ( k + 1 ) ) )
19 ifpfal 
 |-  ( -. ( 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 ) ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
20 18 19 sylbi 
 |-  ( ( 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 ) ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
21 20 biimpar 
 |-  ( ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
22 21 ralimi 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) -> 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 ) ) ) )
23 22 3ad2ant3 
 |-  ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) -> 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 ) ) ) )
24 23 adantl 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) -> 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 ) ) ) )
25 2 1 iswlkg 
 |-  ( G e. W -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ 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 ) ) ) ) ) )
26 25 ad2antrr 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ 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 ) ) ) ) ) )
27 16 17 24 26 mpbir3and 
 |-  ( ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) /\ ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) -> F ( Walks ` G ) P )
28 15 27 impbida 
 |-  ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )