Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> A e. dom vol ) |
2 |
|
mblss |
|- ( A e. dom vol -> A C_ RR ) |
3 |
1 2
|
syl |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> A C_ RR ) |
4 |
|
simpl2 |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> B e. dom vol ) |
5 |
|
mblss |
|- ( B e. dom vol -> B C_ RR ) |
6 |
4 5
|
syl |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> B C_ RR ) |
7 |
3 6
|
unssd |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( A u. B ) C_ RR ) |
8 |
|
readdcl |
|- ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR ) |
9 |
8
|
adantl |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR ) |
10 |
|
simprl |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` A ) e. RR ) |
11 |
|
simprr |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` B ) e. RR ) |
12 |
|
ovolun |
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) ) |
13 |
3 10 6 11 12
|
syl22anc |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) ) |
14 |
|
ovollecl |
|- ( ( ( A u. B ) C_ RR /\ ( ( vol* ` A ) + ( vol* ` B ) ) e. RR /\ ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) ) -> ( vol* ` ( A u. B ) ) e. RR ) |
15 |
7 9 13 14
|
syl3anc |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) e. RR ) |
16 |
|
mblsplit |
|- ( ( A e. dom vol /\ ( A u. B ) C_ RR /\ ( vol* ` ( A u. B ) ) e. RR ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) ) |
17 |
1 7 15 16
|
syl3anc |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) ) |
18 |
|
simpl3 |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( A i^i B ) = (/) ) |
19 |
|
indir |
|- ( ( A u. B ) i^i A ) = ( ( A i^i A ) u. ( B i^i A ) ) |
20 |
|
inidm |
|- ( A i^i A ) = A |
21 |
|
incom |
|- ( B i^i A ) = ( A i^i B ) |
22 |
20 21
|
uneq12i |
|- ( ( A i^i A ) u. ( B i^i A ) ) = ( A u. ( A i^i B ) ) |
23 |
|
unabs |
|- ( A u. ( A i^i B ) ) = A |
24 |
22 23
|
eqtri |
|- ( ( A i^i A ) u. ( B i^i A ) ) = A |
25 |
19 24
|
eqtri |
|- ( ( A u. B ) i^i A ) = A |
26 |
25
|
a1i |
|- ( ( A i^i B ) = (/) -> ( ( A u. B ) i^i A ) = A ) |
27 |
26
|
fveq2d |
|- ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) i^i A ) ) = ( vol* ` A ) ) |
28 |
|
uncom |
|- ( A u. B ) = ( B u. A ) |
29 |
28
|
difeq1i |
|- ( ( A u. B ) \ A ) = ( ( B u. A ) \ A ) |
30 |
|
difun2 |
|- ( ( B u. A ) \ A ) = ( B \ A ) |
31 |
29 30
|
eqtri |
|- ( ( A u. B ) \ A ) = ( B \ A ) |
32 |
21
|
eqeq1i |
|- ( ( B i^i A ) = (/) <-> ( A i^i B ) = (/) ) |
33 |
|
disj3 |
|- ( ( B i^i A ) = (/) <-> B = ( B \ A ) ) |
34 |
32 33
|
sylbb1 |
|- ( ( A i^i B ) = (/) -> B = ( B \ A ) ) |
35 |
31 34
|
eqtr4id |
|- ( ( A i^i B ) = (/) -> ( ( A u. B ) \ A ) = B ) |
36 |
35
|
fveq2d |
|- ( ( A i^i B ) = (/) -> ( vol* ` ( ( A u. B ) \ A ) ) = ( vol* ` B ) ) |
37 |
27 36
|
oveq12d |
|- ( ( A i^i B ) = (/) -> ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) |
38 |
18 37
|
syl |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` ( ( A u. B ) i^i A ) ) + ( vol* ` ( ( A u. B ) \ A ) ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) |
39 |
17 38
|
eqtrd |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) |
40 |
39
|
ex |
|- ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) ) |
41 |
|
mblvol |
|- ( A e. dom vol -> ( vol ` A ) = ( vol* ` A ) ) |
42 |
41
|
eleq1d |
|- ( A e. dom vol -> ( ( vol ` A ) e. RR <-> ( vol* ` A ) e. RR ) ) |
43 |
|
mblvol |
|- ( B e. dom vol -> ( vol ` B ) = ( vol* ` B ) ) |
44 |
43
|
eleq1d |
|- ( B e. dom vol -> ( ( vol ` B ) e. RR <-> ( vol* ` B ) e. RR ) ) |
45 |
42 44
|
bi2anan9 |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) <-> ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) ) |
46 |
45
|
3adant3 |
|- ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) <-> ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) ) ) |
47 |
|
unmbl |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( A u. B ) e. dom vol ) |
48 |
|
mblvol |
|- ( ( A u. B ) e. dom vol -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) ) |
49 |
47 48
|
syl |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( vol ` ( A u. B ) ) = ( vol* ` ( A u. B ) ) ) |
50 |
41 43
|
oveqan12d |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` A ) + ( vol ` B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) |
51 |
49 50
|
eqeq12d |
|- ( ( A e. dom vol /\ B e. dom vol ) -> ( ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) <-> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) ) |
52 |
51
|
3adant3 |
|- ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) <-> ( vol* ` ( A u. B ) ) = ( ( vol* ` A ) + ( vol* ` B ) ) ) ) |
53 |
40 46 52
|
3imtr4d |
|- ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) -> ( ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) -> ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) ) ) |
54 |
53
|
imp |
|- ( ( ( A e. dom vol /\ B e. dom vol /\ ( A i^i B ) = (/) ) /\ ( ( vol ` A ) e. RR /\ ( vol ` B ) e. RR ) ) -> ( vol ` ( A u. B ) ) = ( ( vol ` A ) + ( vol ` B ) ) ) |