Step |
Hyp |
Ref |
Expression |
1 |
|
reex |
|- RR e. _V |
2 |
1
|
elpw2 |
|- ( B e. ~P RR <-> B C_ RR ) |
3 |
|
ismbl |
|- ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) ) |
4 |
|
fveq2 |
|- ( x = B -> ( vol* ` x ) = ( vol* ` B ) ) |
5 |
4
|
eleq1d |
|- ( x = B -> ( ( vol* ` x ) e. RR <-> ( vol* ` B ) e. RR ) ) |
6 |
|
ineq1 |
|- ( x = B -> ( x i^i A ) = ( B i^i A ) ) |
7 |
6
|
fveq2d |
|- ( x = B -> ( vol* ` ( x i^i A ) ) = ( vol* ` ( B i^i A ) ) ) |
8 |
|
difeq1 |
|- ( x = B -> ( x \ A ) = ( B \ A ) ) |
9 |
8
|
fveq2d |
|- ( x = B -> ( vol* ` ( x \ A ) ) = ( vol* ` ( B \ A ) ) ) |
10 |
7 9
|
oveq12d |
|- ( x = B -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) |
11 |
4 10
|
eqeq12d |
|- ( x = B -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) |
12 |
5 11
|
imbi12d |
|- ( x = B -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) ) |
13 |
12
|
rspccv |
|- ( A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) -> ( B e. ~P RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) ) |
14 |
3 13
|
simplbiim |
|- ( A e. dom vol -> ( B e. ~P RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) ) |
15 |
2 14
|
syl5bir |
|- ( A e. dom vol -> ( B C_ RR -> ( ( vol* ` B ) e. RR -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) ) ) |
16 |
15
|
3imp |
|- ( ( A e. dom vol /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` B ) = ( ( vol* ` ( B i^i A ) ) + ( vol* ` ( B \ A ) ) ) ) |