Metamath Proof Explorer

Theorem wlkd

Description: Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses wlkd.p 
|- ( ph -> P e. Word _V )
wlkd.f 
|- ( ph -> F e. Word _V )
wlkd.l 
|- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
wlkd.e 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
wlkd.n 
|- ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
wlkd.g 
|- ( ph -> G e. W )
wlkd.v 
|- V = ( Vtx ` G )
wlkd.i 
|- I = ( iEdg ` G )
wlkd.a 
|- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
Assertion wlkd 
|- ( ph -> F ( Walks ` G ) P )

Proof

Step Hyp Ref Expression
1 wlkd.p 
 |-  ( ph -> P e. Word _V )
2 wlkd.f 
 |-  ( ph -> F e. Word _V )
3 wlkd.l 
 |-  ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )
4 wlkd.e 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
5 wlkd.n 
 |-  ( ph -> A. k e. ( 0 ..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
6 wlkd.g 
 |-  ( ph -> G e. W )
7 wlkd.v 
 |-  V = ( Vtx ` G )
8 wlkd.i 
 |-  I = ( iEdg ` G )
9 wlkd.a 
 |-  ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )
10 1 2 3 4 wlkdlem3 
 |-  ( ph -> F e. Word dom I )
11 1 2 3 9 wlkdlem1 
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
12 1 2 3 4 5 wlkdlem4 
 |-  ( ph -> 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 ) ) ) )
13 7 8 iswlk 
 |-  ( ( G e. W /\ F e. Word _V /\ P e. Word _V ) -> ( 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 ) ) ) ) ) )
14 6 2 1 13 syl3anc 
 |-  ( ph -> ( 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 ) ) ) ) ) )
15 10 11 12 14 mpbir3and 
 |-  ( ph -> F ( Walks ` G ) P )