Step |
Hyp |
Ref |
Expression |
1 |
|
simpl1 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐴 ∈ dom vol ) |
2 |
|
mblss |
⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ ) |
3 |
1 2
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐴 ⊆ ℝ ) |
4 |
|
simpl2 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ∈ dom vol ) |
5 |
|
mblss |
⊢ ( 𝐵 ∈ dom vol → 𝐵 ⊆ ℝ ) |
6 |
4 5
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → 𝐵 ⊆ ℝ ) |
7 |
3 6
|
unssd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ) |
8 |
|
readdcl |
⊢ ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) |
9 |
8
|
adantl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) |
10 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ 𝐴 ) ∈ ℝ ) |
11 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ 𝐵 ) ∈ ℝ ) |
12 |
|
ovolun |
⊢ ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
13 |
3 10 6 11 12
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
14 |
|
ovollecl |
⊢ ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ∧ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ∧ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ ) |
15 |
7 9 13 14
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ ) |
16 |
|
mblsplit |
⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) ) ) ) |
17 |
1 7 15 16
|
syl3anc |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) ) ) ) |
18 |
|
simpl3 |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴 ∩ 𝐵 ) = ∅ ) |
19 |
|
indir |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) = ( ( 𝐴 ∩ 𝐴 ) ∪ ( 𝐵 ∩ 𝐴 ) ) |
20 |
|
inidm |
⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴 |
21 |
|
incom |
⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐴 ∩ 𝐵 ) |
22 |
20 21
|
uneq12i |
⊢ ( ( 𝐴 ∩ 𝐴 ) ∪ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐴 ∪ ( 𝐴 ∩ 𝐵 ) ) |
23 |
|
unabs |
⊢ ( 𝐴 ∪ ( 𝐴 ∩ 𝐵 ) ) = 𝐴 |
24 |
22 23
|
eqtri |
⊢ ( ( 𝐴 ∩ 𝐴 ) ∪ ( 𝐵 ∩ 𝐴 ) ) = 𝐴 |
25 |
19 24
|
eqtri |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) = 𝐴 |
26 |
25
|
a1i |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) = 𝐴 ) |
27 |
26
|
fveq2d |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) ) = ( vol* ‘ 𝐴 ) ) |
28 |
|
uncom |
⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐵 ∪ 𝐴 ) |
29 |
28
|
difeq1i |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) = ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) |
30 |
|
difun2 |
⊢ ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) |
31 |
29 30
|
eqtri |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) |
32 |
21
|
eqeq1i |
⊢ ( ( 𝐵 ∩ 𝐴 ) = ∅ ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) |
33 |
|
disj3 |
⊢ ( ( 𝐵 ∩ 𝐴 ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ 𝐴 ) ) |
34 |
32 33
|
sylbb1 |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → 𝐵 = ( 𝐵 ∖ 𝐴 ) ) |
35 |
31 34
|
eqtr4id |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) = 𝐵 ) |
36 |
35
|
fveq2d |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) ) = ( vol* ‘ 𝐵 ) ) |
37 |
27 36
|
oveq12d |
⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
38 |
18 37
|
syl |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∩ 𝐴 ) ) + ( vol* ‘ ( ( 𝐴 ∪ 𝐵 ) ∖ 𝐴 ) ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
39 |
17 38
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
40 |
39
|
ex |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) ) |
41 |
|
mblvol |
⊢ ( 𝐴 ∈ dom vol → ( vol ‘ 𝐴 ) = ( vol* ‘ 𝐴 ) ) |
42 |
41
|
eleq1d |
⊢ ( 𝐴 ∈ dom vol → ( ( vol ‘ 𝐴 ) ∈ ℝ ↔ ( vol* ‘ 𝐴 ) ∈ ℝ ) ) |
43 |
|
mblvol |
⊢ ( 𝐵 ∈ dom vol → ( vol ‘ 𝐵 ) = ( vol* ‘ 𝐵 ) ) |
44 |
43
|
eleq1d |
⊢ ( 𝐵 ∈ dom vol → ( ( vol ‘ 𝐵 ) ∈ ℝ ↔ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) |
45 |
42 44
|
bi2anan9 |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ) |
46 |
45
|
3adant3 |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ↔ ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ) |
47 |
|
unmbl |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∪ 𝐵 ) ∈ dom vol ) |
48 |
|
mblvol |
⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
49 |
47 48
|
syl |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
50 |
41 43
|
oveqan12d |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) |
51 |
49 50
|
eqeq12d |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ↔ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) ) |
52 |
51
|
3adant3 |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ↔ ( vol* ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ) ) |
53 |
40 46 52
|
3imtr4d |
⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) → ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ) ) |
54 |
53
|
imp |
⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ ( ( vol ‘ 𝐴 ) ∈ ℝ ∧ ( vol ‘ 𝐵 ) ∈ ℝ ) ) → ( vol ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( vol ‘ 𝐴 ) + ( vol ‘ 𝐵 ) ) ) |