Metamath Proof Explorer

Theorem upwlkwlk

Description: A simple walk is a walk. (Contributed by AV, 30-Dec-2020) (Proof shortened by AV, 27-Feb-2021)

Ref Expression
Assertion upwlkwlk 
|- ( F ( UPWalks ` G ) P -> F ( Walks ` G ) P )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
2 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
3 1 2 upwlkbprop 
 |-  ( F ( UPWalks ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
4 idd 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F e. Word dom ( iEdg ` G ) -> F e. Word dom ( iEdg ` G ) ) )
5 idd 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
6 ifpprsnss 
 |-  ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) )
7 6 a1i 
 |-  ( ( ( G e. _V /\ F e. _V /\ P e. _V ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
8 7 ralimdva 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
9 4 5 8 3anim123d 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
10 1 2 isupwlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( UPWalks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
11 1 2 iswlk 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
12 9 10 11 3imtr4d 
 |-  ( ( G e. _V /\ F e. _V /\ P e. _V ) -> ( F ( UPWalks ` G ) P -> F ( Walks ` G ) P ) )
13 3 12 mpcom 
 |-  ( F ( UPWalks ` G ) P -> F ( Walks ` G ) P )