Proof of Theorem volun
Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐴 ∈
dom vol) |
2 | | mblss 23299 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐴 ⊆
ℝ) |
4 | | simpl2 1065 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐵 ∈
dom vol) |
5 | | mblss 23299 |
. . . . . . . 8
⊢ (𝐵 ∈ dom vol → 𝐵 ⊆
ℝ) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐵 ⊆
ℝ) |
7 | 3, 6 | unssd 3789 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (𝐴 ∪
𝐵) ⊆
ℝ) |
8 | | readdcl 10019 |
. . . . . . . 8
⊢
(((vol*‘𝐴)
∈ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) |
9 | 8 | adantl 482 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ) |
10 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘𝐴) ∈ ℝ) |
11 | | simprr 796 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘𝐵) ∈ ℝ) |
12 | | ovolun 23267 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (𝐵 ⊆
ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) |
13 | 3, 10, 6, 11, 12 | syl22anc 1327 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) |
14 | | ovollecl 23251 |
. . . . . . 7
⊢ (((𝐴 ∪ 𝐵) ⊆ ℝ ∧ ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ ∧
(vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) |
15 | 7, 9, 13, 14 | syl3anc 1326 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) |
16 | | mblsplit 23300 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ∪ 𝐵) ⊆ ℝ ∧ (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)))) |
17 | 1, 7, 15, 16 | syl3anc 1326 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)))) |
18 | | simpl3 1066 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (𝐴 ∩
𝐵) =
∅) |
19 | | indir 3875 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐴) = ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) |
20 | | inidm 3822 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐴) = 𝐴 |
21 | | incom 3805 |
. . . . . . . . . . . 12
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) |
22 | 20, 21 | uneq12i 3765 |
. . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) = (𝐴 ∪ (𝐴 ∩ 𝐵)) |
23 | | unabs 3854 |
. . . . . . . . . . 11
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 |
24 | 22, 23 | eqtri 2644 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) = 𝐴 |
25 | 19, 24 | eqtri 2644 |
. . . . . . . . 9
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐴) = 𝐴 |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∩ 𝐴) = 𝐴) |
27 | 26 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) = ∅ → (vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) = (vol*‘𝐴)) |
28 | 21 | eqeq1i 2627 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅) |
29 | | disj3 4021 |
. . . . . . . . . . 11
⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴)) |
30 | 28, 29 | bitr3i 266 |
. . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴)) |
31 | 30 | biimpi 206 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) = ∅ → 𝐵 = (𝐵 ∖ 𝐴)) |
32 | | uncom 3757 |
. . . . . . . . . . 11
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) |
33 | 32 | difeq1i 3724 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) |
34 | | difun2 4048 |
. . . . . . . . . 10
⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴) |
35 | 33, 34 | eqtri 2644 |
. . . . . . . . 9
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐴) = (𝐵 ∖ 𝐴) |
36 | 31, 35 | syl6reqr 2675 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐴) = 𝐵) |
37 | 36 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) = ∅ → (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)) = (vol*‘𝐵)) |
38 | 27, 37 | oveq12d 6668 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴))) = ((vol*‘𝐴) + (vol*‘𝐵))) |
39 | 18, 38 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴))) = ((vol*‘𝐴) + (vol*‘𝐵))) |
40 | 17, 39 | eqtrd 2656 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵))) |
41 | 40 | ex 450 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) |
42 | | mblvol 23298 |
. . . . . 6
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
43 | 42 | eleq1d 2686 |
. . . . 5
⊢ (𝐴 ∈ dom vol →
((vol‘𝐴) ∈
ℝ ↔ (vol*‘𝐴) ∈ ℝ)) |
44 | | mblvol 23298 |
. . . . . 6
⊢ (𝐵 ∈ dom vol →
(vol‘𝐵) =
(vol*‘𝐵)) |
45 | 44 | eleq1d 2686 |
. . . . 5
⊢ (𝐵 ∈ dom vol →
((vol‘𝐵) ∈
ℝ ↔ (vol*‘𝐵) ∈ ℝ)) |
46 | 43, 45 | bi2anan9 917 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
(((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ) ↔ ((vol*‘𝐴) ∈ ℝ ∧ (vol*‘𝐵) ∈
ℝ))) |
47 | 46 | 3adant3 1081 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ) ↔ ((vol*‘𝐴) ∈ ℝ ∧ (vol*‘𝐵) ∈
ℝ))) |
48 | | unmbl 23305 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) |
49 | | mblvol 23298 |
. . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom vol → (vol‘(𝐴 ∪ 𝐵)) = (vol*‘(𝐴 ∪ 𝐵))) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
(vol‘(𝐴 ∪ 𝐵)) = (vol*‘(𝐴 ∪ 𝐵))) |
51 | 42, 44 | oveqan12d 6669 |
. . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
((vol‘𝐴) +
(vol‘𝐵)) =
((vol*‘𝐴) +
(vol*‘𝐵))) |
52 | 50, 51 | eqeq12d 2637 |
. . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
((vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)) ↔ (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) |
53 | 52 | 3adant3 1081 |
. . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → ((vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)) ↔ (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) |
54 | 41, 47, 53 | 3imtr4d 283 |
. 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)))) |
55 | 54 | imp 445 |
1
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ)) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵))) |