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