Metamath Proof Explorer

Theorem ewlkprop

Description: Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i 
|- I = ( iEdg ` G )
Assertion ewlkprop 
|- ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i 
 |-  I = ( iEdg ` G )
2 df-ewlks 
 |-  EdgWalks = ( g e. _V , s e. NN0* |-> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } )
3 2 elmpocl 
 |-  ( F e. ( G EdgWalks S ) -> ( G e. _V /\ S e. NN0* ) )
4 simpr 
 |-  ( ( F e. ( G EdgWalks S ) /\ ( G e. _V /\ S e. NN0* ) ) -> ( G e. _V /\ S e. NN0* ) )
5 1 isewlk 
 |-  ( ( G e. _V /\ S e. NN0* /\ F e. ( G EdgWalks S ) ) -> ( F e. ( G EdgWalks S ) <-> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
6 5 3expa 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. ( G EdgWalks S ) ) -> ( F e. ( G EdgWalks S ) <-> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
7 6 biimpd 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. ( G EdgWalks S ) ) -> ( F e. ( G EdgWalks S ) -> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
8 7 expcom 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) -> ( F e. ( G EdgWalks S ) -> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) ) )
9 8 pm2.43a 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) -> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
10 9 imp 
 |-  ( ( F e. ( G EdgWalks S ) /\ ( G e. _V /\ S e. NN0* ) ) -> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )
11 3anass 
 |-  ( ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) <-> ( ( G e. _V /\ S e. NN0* ) /\ ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
12 4 10 11 sylanbrc 
 |-  ( ( F e. ( G EdgWalks S ) /\ ( G e. _V /\ S e. NN0* ) ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )
13 3 12 mpdan 
 |-  ( F e. ( G EdgWalks S ) -> ( ( G e. _V /\ S e. NN0* ) /\ F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )