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 ) ) ) ) ) } )