Metamath Proof Explorer

Theorem ewlksfval

Description: The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021)

Ref Expression
Hypothesis ewlksfval.i 
|- I = ( iEdg ` G )
Assertion 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 ) ) ) ) ) } )

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 a1i 
 |-  ( ( G e. W /\ S e. NN0* ) -> 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 ) ) ) ) ) } ) )
4 fvexd 
 |-  ( ( g = G /\ s = S ) -> ( iEdg ` g ) e. _V )
5 simpr 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> i = ( iEdg ` g ) )
6 fveq2 
 |-  ( g = G -> ( iEdg ` g ) = ( iEdg ` G ) )
7 6 adantr 
 |-  ( ( g = G /\ s = S ) -> ( iEdg ` g ) = ( iEdg ` G ) )
8 7 adantr 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( iEdg ` g ) = ( iEdg ` G ) )
9 5 8 eqtrd 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> i = ( iEdg ` G ) )
10 9 dmeqd 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> dom i = dom ( iEdg ` G ) )
11 wrdeq 
 |-  ( dom i = dom ( iEdg ` G ) -> Word dom i = Word dom ( iEdg ` G ) )
12 10 11 syl 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> Word dom i = Word dom ( iEdg ` G ) )
13 12 eleq2d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( f e. Word dom i <-> f e. Word dom ( iEdg ` G ) ) )
14 simpr 
 |-  ( ( g = G /\ s = S ) -> s = S )
15 14 adantr 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> s = S )
16 9 fveq1d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( i ` ( f ` ( k - 1 ) ) ) = ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) )
17 9 fveq1d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( i ` ( f ` k ) ) = ( ( iEdg ` G ) ` ( f ` k ) ) )
18 16 17 ineq12d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) = ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) )
19 18 fveq2d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) = ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) )
20 15 19 breq12d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) <-> S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) )
21 20 ralbidv 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) <-> A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) )
22 13 21 anbi12d 
 |-  ( ( ( g = G /\ s = S ) /\ i = ( iEdg ` g ) ) -> ( ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) <-> ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) ) )
23 4 22 sbcied 
 |-  ( ( g = G /\ s = S ) -> ( [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) <-> ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) ) )
24 23 abbidv 
 |-  ( ( g = G /\ s = S ) -> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } = { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) } )
25 24 adantl 
 |-  ( ( ( G e. W /\ S e. NN0* ) /\ ( g = G /\ s = S ) ) -> { f | [. ( iEdg ` g ) / i ]. ( f e. Word dom i /\ A. k e. ( 1 ..^ ( # ` f ) ) s <_ ( # ` ( ( i ` ( f ` ( k - 1 ) ) ) i^i ( i ` ( f ` k ) ) ) ) ) } = { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) } )
26 elex 
 |-  ( G e. W -> G e. _V )
27 26 adantr 
 |-  ( ( G e. W /\ S e. NN0* ) -> G e. _V )
28 simpr 
 |-  ( ( G e. W /\ S e. NN0* ) -> S e. NN0* )
29 df-rab 
 |-  { f e. Word dom ( iEdg ` G ) | A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) } = { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) }
30 fvex 
 |-  ( iEdg ` G ) e. _V
31 30 dmex 
 |-  dom ( iEdg ` G ) e. _V
32 31 wrdexi 
 |-  Word dom ( iEdg ` G ) e. _V
33 32 rabex 
 |-  { f e. Word dom ( iEdg ` G ) | A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) } e. _V
34 33 a1i 
 |-  ( ( G e. W /\ S e. NN0* ) -> { f e. Word dom ( iEdg ` G ) | A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) } e. _V )
35 29 34 eqeltrrid 
 |-  ( ( G e. W /\ S e. NN0* ) -> { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) } e. _V )
36 3 25 27 28 35 ovmpod 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( G EdgWalks S ) = { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) } )
37 1 eqcomi 
 |-  ( iEdg ` G ) = I
38 37 a1i 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( iEdg ` G ) = I )
39 38 dmeqd 
 |-  ( ( G e. W /\ S e. NN0* ) -> dom ( iEdg ` G ) = dom I )
40 wrdeq 
 |-  ( dom ( iEdg ` G ) = dom I -> Word dom ( iEdg ` G ) = Word dom I )
41 39 40 syl 
 |-  ( ( G e. W /\ S e. NN0* ) -> Word dom ( iEdg ` G ) = Word dom I )
42 41 eleq2d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( f e. Word dom ( iEdg ` G ) <-> f e. Word dom I ) )
43 38 fveq1d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) = ( I ` ( f ` ( k - 1 ) ) ) )
44 38 fveq1d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( ( iEdg ` G ) ` ( f ` k ) ) = ( I ` ( f ` k ) ) )
45 43 44 ineq12d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) = ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) )
46 45 fveq2d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) = ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) )
47 46 breq2d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) <-> S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) )
48 47 ralbidv 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) <-> A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) )
49 42 48 anbi12d 
 |-  ( ( G e. W /\ S e. NN0* ) -> ( ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) <-> ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) ) )
50 49 abbidv 
 |-  ( ( G e. W /\ S e. NN0* ) -> { f | ( f e. Word dom ( iEdg ` G ) /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( ( iEdg ` G ) ` ( f ` ( k - 1 ) ) ) i^i ( ( iEdg ` G ) ` ( f ` k ) ) ) ) ) } = { f | ( f e. Word dom I /\ A. k e. ( 1 ..^ ( # ` f ) ) S <_ ( # ` ( ( I ` ( f ` ( k - 1 ) ) ) i^i ( I ` ( f ` k ) ) ) ) ) } )
51 36 50 eqtrd 
 |-  ( ( 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 ) ) ) ) ) } )