Metamath Proof Explorer

Theorem isewlk

Description: Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i 
|- I = ( iEdg ` G )
Assertion isewlk 
|- ( ( G e. W /\ S e. NN0* /\ F e. U ) -> ( 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ewlksfval.i 
 |-  I = ( iEdg ` G )
2 1 ewlksfval 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( G EdgWalks S ) = { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } )
3 2 3adant3 
 |-  ( ( G e. W /\ S e. NN0* /\ F e. U ) -> ( G EdgWalks S ) = { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } )
4 3 eleq2d 
 |-  ( ( G e. W /\ S e. NN0* /\ F e. U ) -> ( F e. ( G EdgWalks S ) <-> F e. { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } ) )
5 eleq1 
 |-  ( f = F -> ( f e. Word dom I <-> F e. Word dom I ) )
6 fveq2 
 |-  ( f = F -> ( # ` f ) = ( # ` F ) )
7 6 oveq2d 
 |-  ( f = F -> ( 1 ..^ ( # ` f ) ) = ( 1 ..^ ( # ` F ) ) )
8 fveq1 
 |-  ( f = F -> ( f ` ( k - 1 ) ) = ( F ` ( k - 1 ) ) )
9 8 fveq2d 
 |-  ( f = F -> ( I ` ( f ` ( k - 1 ) ) ) = ( I ` ( F ` ( k - 1 ) ) ) )
10 fveq1 
 |-  ( f = F -> ( f ` k ) = ( F ` k ) )
11 10 fveq2d 
 |-  ( f = F -> ( I ` ( f ` k ) ) = ( I ` ( F ` k ) ) )
12 9 11 ineq12d 
 |-  ( f = F -> ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) = ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) )
13 12 fveq2d 
 |-  ( f = F -> ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) = ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) )
14 13 breq2d 
 |-  ( f = F -> ( S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) <-> S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )
15 7 14 raleqbidv 
 |-  ( f = F -> ( A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) <-> A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) )
16 5 15 anbi12d 
 |-  ( f = F -> ( ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) <-> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
17 16 elabg 
 |-  ( F e. U -> ( F e. { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } <-> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
18 17 3ad2ant3 
 |-  ( ( G e. W /\ S e. NN0* /\ F e. U ) -> ( F e. { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } <-> ( F e. Word dom I /\ A. k e. ( 1 ..^ ( # ` F ) ) S <_ ( # ` ( ( I ` ( F ` ( k - 1 ) ) ) i^i ( I ` ( F ` k ) ) ) ) ) ) )
19 4 18 bitrd 
 |-  ( ( G e. W /\ S e. NN0* /\ F e. U ) -> ( 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 ) ) ) ) ) ) )