Step | Hyp | Ref
| Expression |
1 | | mblss 23106 |
. . . 4
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
2 | | mblss 23106 |
. . . 4
⊢ (𝐵 ∈ dom vol → 𝐵 ⊆
ℝ) |
3 | 1, 2 | anim12i 588 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ⊆ ℝ ∧ 𝐵 ⊆
ℝ)) |
4 | | unss 3749 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ) ↔ (𝐴 ∪ 𝐵) ⊆ ℝ) |
5 | 3, 4 | sylib 207 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ⊆ ℝ) |
6 | | elpwi 4117 |
. . . 4
⊢ (𝑥 ∈ 𝒫 ℝ →
𝑥 ⊆
ℝ) |
7 | | inss1 3795 |
. . . . . . . . 9
⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) ⊆ 𝑥 |
8 | | ovolsscl 23061 |
. . . . . . . . 9
⊢ (((𝑥 ∩ (𝐴 ∪ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ) |
9 | 7, 8 | mp3an1 1403 |
. . . . . . . 8
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ∈ ℝ) |
11 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑥 ∩ 𝐴) ⊆ 𝑥 |
12 | | ovolsscl 23061 |
. . . . . . . . . 10
⊢ (((𝑥 ∩ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∩ 𝐴)) ∈
ℝ) |
13 | 11, 12 | mp3an1 1403 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
14 | 13 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) |
15 | | difss 3699 |
. . . . . . . . . 10
⊢ (𝑥 ∖ 𝐴) ⊆ 𝑥 |
16 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → 𝑥 ⊆
ℝ) |
17 | 15, 16 | syl5ss 3579 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∖
𝐴) ⊆
ℝ) |
18 | | ovolsscl 23061 |
. . . . . . . . . . 11
⊢ (((𝑥 ∖ 𝐴) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
𝐴)) ∈
ℝ) |
19 | 15, 18 | mp3an1 1403 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
20 | 19 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) |
21 | | inss1 3795 |
. . . . . . . . . 10
⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∖ 𝐴) |
22 | | ovolsscl 23061 |
. . . . . . . . . 10
⊢ ((((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∖ 𝐴) ∧ (𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) →
(vol*‘((𝑥 ∖
𝐴) ∩ 𝐵)) ∈ ℝ) |
23 | 21, 22 | mp3an1 1403 |
. . . . . . . . 9
⊢ (((𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) →
(vol*‘((𝑥 ∖
𝐴) ∩ 𝐵)) ∈ ℝ) |
24 | 17, 20, 23 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℝ) |
25 | 14, 24 | readdcld 9948 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) ∈ ℝ) |
26 | | difss 3699 |
. . . . . . . . 9
⊢ (𝑥 ∖ (𝐴 ∪ 𝐵)) ⊆ 𝑥 |
27 | | ovolsscl 23061 |
. . . . . . . . 9
⊢ (((𝑥 ∖ (𝐴 ∪ 𝐵)) ⊆ 𝑥 ∧ 𝑥 ⊆ ℝ ∧ (vol*‘𝑥) ∈ ℝ) →
(vol*‘(𝑥 ∖
(𝐴 ∪ 𝐵))) ∈ ℝ) |
28 | 26, 27 | mp3an1 1403 |
. . . . . . . 8
⊢ ((𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℝ) |
29 | 28 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℝ) |
30 | | incom 3767 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) = (𝐵 ∩ (𝑥 ∖ 𝐴)) |
31 | | indifcom 3831 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ (𝑥 ∖ 𝐴)) = (𝑥 ∩ (𝐵 ∖ 𝐴)) |
32 | 30, 31 | eqtri 2632 |
. . . . . . . . . . 11
⊢ ((𝑥 ∖ 𝐴) ∩ 𝐵) = (𝑥 ∩ (𝐵 ∖ 𝐴)) |
33 | 32 | uneq2i 3726 |
. . . . . . . . . 10
⊢ ((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ (𝐵 ∖ 𝐴))) |
34 | | indi 3832 |
. . . . . . . . . 10
⊢ (𝑥 ∩ (𝐴 ∪ (𝐵 ∖ 𝐴))) = ((𝑥 ∩ 𝐴) ∪ (𝑥 ∩ (𝐵 ∖ 𝐴))) |
35 | | undif2 3996 |
. . . . . . . . . . 11
⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵) |
36 | 35 | ineq2i 3773 |
. . . . . . . . . 10
⊢ (𝑥 ∩ (𝐴 ∪ (𝐵 ∖ 𝐴))) = (𝑥 ∩ (𝐴 ∪ 𝐵)) |
37 | 33, 34, 36 | 3eqtr2ri 2639 |
. . . . . . . . 9
⊢ (𝑥 ∩ (𝐴 ∪ 𝐵)) = ((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵)) |
38 | 37 | fveq2i 6106 |
. . . . . . . 8
⊢
(vol*‘(𝑥 ∩
(𝐴 ∪ 𝐵))) = (vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))) |
39 | 11, 16 | syl5ss 3579 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (𝑥 ∩
𝐴) ⊆
ℝ) |
40 | 21, 17 | syl5ss 3579 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((𝑥
∖ 𝐴) ∩ 𝐵) ⊆
ℝ) |
41 | | ovolun 23074 |
. . . . . . . . 9
⊢ ((((𝑥 ∩ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∩ 𝐴)) ∈ ℝ) ∧ (((𝑥 ∖ 𝐴) ∩ 𝐵) ⊆ ℝ ∧ (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℝ)) →
(vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)))) |
42 | 39, 14, 40, 24, 41 | syl22anc 1319 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘((𝑥 ∩ 𝐴) ∪ ((𝑥 ∖ 𝐴) ∩ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)))) |
43 | 38, 42 | syl5eqbr 4618 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) ≤ ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)))) |
44 | 10, 25, 29, 43 | leadd1dd 10520 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))))) |
45 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → 𝐵 ∈
dom vol) |
46 | | mblsplit 23107 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ dom vol ∧ (𝑥 ∖ 𝐴) ⊆ ℝ ∧ (vol*‘(𝑥 ∖ 𝐴)) ∈ ℝ) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵)))) |
47 | 45, 17, 20, 46 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵)))) |
48 | | difun1 3846 |
. . . . . . . . . . 11
⊢ (𝑥 ∖ (𝐴 ∪ 𝐵)) = ((𝑥 ∖ 𝐴) ∖ 𝐵) |
49 | 48 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(vol*‘(𝑥
∖ (𝐴 ∪ 𝐵))) = (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵)) |
50 | 49 | oveq2i 6560 |
. . . . . . . . 9
⊢
((vol*‘((𝑥
∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘((𝑥 ∖ 𝐴) ∖ 𝐵))) |
51 | 47, 50 | syl6eqr 2662 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ 𝐴)) = ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))))) |
52 | 51 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴))) = ((vol*‘(𝑥 ∩ 𝐴)) + ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))))) |
53 | | simpll 786 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → 𝐴 ∈
dom vol) |
54 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) ∈ ℝ) |
55 | | mblsplit 23107 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom vol ∧ 𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
56 | 53, 16, 54, 55 | syl3anc 1318 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) = ((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘(𝑥 ∖ 𝐴)))) |
57 | 14 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∩ 𝐴)) ∈ ℂ) |
58 | 24 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) ∈ ℂ) |
59 | 29 | recnd 9947 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))) ∈ ℂ) |
60 | 57, 58, 59 | addassd 9941 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) = ((vol*‘(𝑥 ∩ 𝐴)) + ((vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵)) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))))) |
61 | 52, 56, 60 | 3eqtr4d 2654 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → (vol*‘𝑥) = (((vol*‘(𝑥 ∩ 𝐴)) + (vol*‘((𝑥 ∖ 𝐴) ∩ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵))))) |
62 | 44, 61 | breqtrrd 4611 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ (𝑥 ⊆ ℝ ∧
(vol*‘𝑥) ∈
ℝ)) → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥)) |
63 | 62 | expr 641 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ 𝑥 ⊆ ℝ) →
((vol*‘𝑥) ∈
ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥))) |
64 | 6, 63 | sylan2 490 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧ 𝑥 ∈ 𝒫 ℝ)
→ ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥))) |
65 | 64 | ralrimiva 2949 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥))) |
66 | | ismbl2 23102 |
. 2
⊢ ((𝐴 ∪ 𝐵) ∈ dom vol ↔ ((𝐴 ∪ 𝐵) ⊆ ℝ ∧ ∀𝑥 ∈ 𝒫
ℝ((vol*‘𝑥)
∈ ℝ → ((vol*‘(𝑥 ∩ (𝐴 ∪ 𝐵))) + (vol*‘(𝑥 ∖ (𝐴 ∪ 𝐵)))) ≤ (vol*‘𝑥)))) |
67 | 5, 65, 66 | sylanbrc 695 |
1
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) |