Step |
Hyp |
Ref |
Expression |
1 |
|
mblss |
|- ( A e. dom vol -> A C_ RR ) |
2 |
|
mblss |
|- ( B e. dom vol -> B C_ RR ) |
3 |
1 2
|
anim12i |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A C_ RR /\ B C_ RR ) ) |
4 |
|
unss |
|- ( ( A C_ RR /\ B C_ RR ) <-> ( A u. B ) C_ RR ) |
5 |
3 4
|
sylib |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) C_ RR ) |
6 |
|
elpwi |
|- ( x e. ~P RR -> x C_ RR ) |
7 |
|
inss1 |
|- ( x i^i ( A u. B ) ) C_ x |
8 |
|
ovolsscl |
|- ( ( ( x i^i ( A u. B ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR ) |
9 |
7 8
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR ) |
10 |
9
|
adantl |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A u. B ) ) ) e. RR ) |
11 |
|
inss1 |
|- ( x i^i A ) C_ x |
12 |
|
ovolsscl |
|- ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
13 |
11 12
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
14 |
13
|
adantl |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. RR ) |
15 |
|
inss1 |
|- ( ( x \ A ) i^i B ) C_ ( x \ A ) |
16 |
|
difss |
|- ( x \ A ) C_ x |
17 |
|
simprl |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> x C_ RR ) |
18 |
16 17
|
sstrid |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x \ A ) C_ RR ) |
19 |
|
ovolsscl |
|- ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
20 |
16 19
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR ) |
21 |
20
|
adantl |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) e. RR ) |
22 |
|
ovolsscl |
|- ( ( ( ( x \ A ) i^i B ) C_ ( x \ A ) /\ ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. RR ) |
23 |
15 18 21 22
|
mp3an2i |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. RR ) |
24 |
14 23
|
readdcld |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) e. RR ) |
25 |
|
difss |
|- ( x \ ( A u. B ) ) C_ x |
26 |
|
ovolsscl |
|- ( ( ( x \ ( A u. B ) ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR ) |
27 |
25 26
|
mp3an1 |
|- ( ( x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR ) |
28 |
27
|
adantl |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. RR ) |
29 |
|
incom |
|- ( ( x \ A ) i^i B ) = ( B i^i ( x \ A ) ) |
30 |
|
indifcom |
|- ( B i^i ( x \ A ) ) = ( x i^i ( B \ A ) ) |
31 |
29 30
|
eqtri |
|- ( ( x \ A ) i^i B ) = ( x i^i ( B \ A ) ) |
32 |
31
|
uneq2i |
|- ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) = ( ( x i^i A ) u. ( x i^i ( B \ A ) ) ) |
33 |
|
indi |
|- ( x i^i ( A u. ( B \ A ) ) ) = ( ( x i^i A ) u. ( x i^i ( B \ A ) ) ) |
34 |
|
undif2 |
|- ( A u. ( B \ A ) ) = ( A u. B ) |
35 |
34
|
ineq2i |
|- ( x i^i ( A u. ( B \ A ) ) ) = ( x i^i ( A u. B ) ) |
36 |
32 33 35
|
3eqtr2ri |
|- ( x i^i ( A u. B ) ) = ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) |
37 |
36
|
fveq2i |
|- ( vol* ` ( x i^i ( A u. B ) ) ) = ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) ) |
38 |
11 17
|
sstrid |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( x i^i A ) C_ RR ) |
39 |
15 18
|
sstrid |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( x \ A ) i^i B ) C_ RR ) |
40 |
|
ovolun |
|- ( ( ( ( x i^i A ) C_ RR /\ ( vol* ` ( x i^i A ) ) e. RR ) /\ ( ( ( x \ A ) i^i B ) C_ RR /\ ( vol* ` ( ( x \ A ) i^i B ) ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) ) |
41 |
38 14 39 23 40
|
syl22anc |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x i^i A ) u. ( ( x \ A ) i^i B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) ) |
42 |
37 41
|
eqbrtrid |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i ( A u. B ) ) ) <_ ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) ) |
43 |
10 24 28 42
|
leadd1dd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) |
44 |
|
simplr |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> B e. dom vol ) |
45 |
|
mblsplit |
|- ( ( B e. dom vol /\ ( x \ A ) C_ RR /\ ( vol* ` ( x \ A ) ) e. RR ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) ) ) |
46 |
44 18 21 45
|
syl3anc |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) ) ) |
47 |
|
difun1 |
|- ( x \ ( A u. B ) ) = ( ( x \ A ) \ B ) |
48 |
47
|
fveq2i |
|- ( vol* ` ( x \ ( A u. B ) ) ) = ( vol* ` ( ( x \ A ) \ B ) ) |
49 |
48
|
oveq2i |
|- ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( ( x \ A ) \ B ) ) ) |
50 |
46 49
|
eqtr4di |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ A ) ) = ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) |
51 |
50
|
oveq2d |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) ) |
52 |
|
simpll |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> A e. dom vol ) |
53 |
|
simprr |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) e. RR ) |
54 |
|
mblsplit |
|- ( ( A e. dom vol /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
55 |
52 17 53 54
|
syl3anc |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) ) |
56 |
14
|
recnd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x i^i A ) ) e. CC ) |
57 |
23
|
recnd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( ( x \ A ) i^i B ) ) e. CC ) |
58 |
28
|
recnd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` ( x \ ( A u. B ) ) ) e. CC ) |
59 |
56 57 58
|
addassd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( ( vol* ` ( ( x \ A ) i^i B ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) ) |
60 |
51 55 59
|
3eqtr4d |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( vol* ` x ) = ( ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( ( x \ A ) i^i B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) ) |
61 |
43 60
|
breqtrrd |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ ( x C_ RR /\ ( vol* ` x ) e. RR ) ) -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) |
62 |
61
|
expr |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ x C_ RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) ) |
63 |
6 62
|
sylan2 |
|- ( ( ( A e. dom vol /\ B e. dom vol ) /\ x e. ~P RR ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) ) |
64 |
63
|
ralrimiva |
|- ( ( A e. dom vol /\ B e. dom vol ) -> A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) ) |
65 |
|
ismbl2 |
|- ( ( A u. B ) e. dom vol <-> ( ( A u. B ) C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i ( A u. B ) ) ) + ( vol* ` ( x \ ( A u. B ) ) ) ) <_ ( vol* ` x ) ) ) ) |
66 |
5 64 65
|
sylanbrc |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol ) |