Step |
Hyp |
Ref |
Expression |
1 |
|
resdmres |
|- ( vol* |` dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) ) = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) |
2 |
|
df-vol |
|- vol = ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) |
3 |
2
|
dmeqi |
|- dom vol = dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) |
4 |
3
|
reseq2i |
|- ( vol* |` dom vol ) = ( vol* |` dom ( vol* |` { x | A. y e. ( `' vol* " RR ) ( vol* ` y ) = ( ( vol* ` ( y i^i x ) ) + ( vol* ` ( y \ x ) ) ) } ) ) |
5 |
1 4 2
|
3eqtr4ri |
|- vol = ( vol* |` dom vol ) |