Step |
Hyp |
Ref |
Expression |
1 |
|
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 ) ) ) ) ) ) |
2 |
|
elpwi |
|- ( x e. ~P RR -> x C_ RR ) |
3 |
|
inundif |
|- ( ( x i^i A ) u. ( x \ A ) ) = x |
4 |
3
|
fveq2i |
|- ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) = ( vol* ` x ) |
5 |
|
inss1 |
|- ( x i^i A ) C_ x |
6 |
|
simprl |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> x C_ RR ) |
7 |
5 6
|
sstrid |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x i^i A ) C_ RR ) |
8 |
|
ovolsscl |
|- ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
9 |
5 8
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
10 |
9
|
adantl |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
11 |
|
difss |
|- ( x \ A ) C_ x |
12 |
11 6
|
sstrid |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x \ A ) C_ RR ) |
13 |
|
ovolsscl |
|- ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
14 |
11 13
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
15 |
14
|
adantl |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. RR ) |
16 |
|
ovolun |
|- ( ( ( ( x i^i A ) C_ RR /\ ( vol* ` ( x i^i A ) ) e. RR ) /\ ( ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
17 |
7 10 12 15 16
|
syl22anc |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
18 |
4 17
|
eqbrtrrid |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
19 |
|
simprr |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR ) |
20 |
10 15
|
readdcld |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) e. RR ) |
21 |
19 20
|
letri3d |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) /\ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
22 |
18 21
|
mpbirand |
|- ( ( A C_ RR /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) |
23 |
22
|
expr |
|- ( ( A C_ RR /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <-> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
24 |
23
|
pm5.74d |
|- ( ( A C_ RR /\ x C_ RR ) -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
25 |
2 24
|
sylan2 |
|- ( ( A C_ RR /\ x e. ~P RR ) -> ( ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
26 |
25
|
ralbidva |
|- ( A C_ RR -> ( A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) <-> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
27 |
26
|
pm5.32i |
|- ( ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) ) <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |
28 |
1 27
|
bitri |
|- ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) ) |