Proof of Theorem volun
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1192 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐴 ∈
dom vol) | 
| 2 |  | mblss 25566 | . . . . . . . 8
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) | 
| 3 | 1, 2 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐴 ⊆
ℝ) | 
| 4 |  | simpl2 1193 | . . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐵 ∈
dom vol) | 
| 5 |  | mblss 25566 | . . . . . . . 8
⊢ (𝐵 ∈ dom vol → 𝐵 ⊆
ℝ) | 
| 6 | 4, 5 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → 𝐵 ⊆
ℝ) | 
| 7 | 3, 6 | unssd 4192 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (𝐴 ∪
𝐵) ⊆
ℝ) | 
| 8 |  | readdcl 11238 | . . . . . . . 8
⊢
(((vol*‘𝐴)
∈ ℝ ∧ (vol*‘𝐵) ∈ ℝ) → ((vol*‘𝐴) + (vol*‘𝐵)) ∈
ℝ) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ) | 
| 10 |  | simprl 771 | . . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘𝐴) ∈ ℝ) | 
| 11 |  | simprr 773 | . . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘𝐵) ∈ ℝ) | 
| 12 |  | ovolun 25534 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧
(vol*‘𝐴) ∈
ℝ) ∧ (𝐵 ⊆
ℝ ∧ (vol*‘𝐵) ∈ ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 13 | 3, 10, 6, 11, 12 | syl22anc 839 | . . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 14 |  | ovollecl 25518 | . . . . . . 7
⊢ (((𝐴 ∪ 𝐵) ⊆ ℝ ∧ ((vol*‘𝐴) + (vol*‘𝐵)) ∈ ℝ ∧
(vol*‘(𝐴 ∪ 𝐵)) ≤ ((vol*‘𝐴) + (vol*‘𝐵))) → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) | 
| 15 | 7, 9, 13, 14 | syl3anc 1373 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) | 
| 16 |  | mblsplit 25567 | . . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ (𝐴 ∪ 𝐵) ⊆ ℝ ∧ (vol*‘(𝐴 ∪ 𝐵)) ∈ ℝ) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)))) | 
| 17 | 1, 7, 15, 16 | syl3anc 1373 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)))) | 
| 18 |  | simpl3 1194 | . . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (𝐴 ∩
𝐵) =
∅) | 
| 19 |  | indir 4286 | . . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐴) = ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) | 
| 20 |  | inidm 4227 | . . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝐴) = 𝐴 | 
| 21 |  | incom 4209 | . . . . . . . . . . . 12
⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | 
| 22 | 20, 21 | uneq12i 4166 | . . . . . . . . . . 11
⊢ ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) = (𝐴 ∪ (𝐴 ∩ 𝐵)) | 
| 23 |  | unabs 4265 | . . . . . . . . . . 11
⊢ (𝐴 ∪ (𝐴 ∩ 𝐵)) = 𝐴 | 
| 24 | 22, 23 | eqtri 2765 | . . . . . . . . . 10
⊢ ((𝐴 ∩ 𝐴) ∪ (𝐵 ∩ 𝐴)) = 𝐴 | 
| 25 | 19, 24 | eqtri 2765 | . . . . . . . . 9
⊢ ((𝐴 ∪ 𝐵) ∩ 𝐴) = 𝐴 | 
| 26 | 25 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∩ 𝐴) = 𝐴) | 
| 27 | 26 | fveq2d 6910 | . . . . . . 7
⊢ ((𝐴 ∩ 𝐵) = ∅ → (vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) = (vol*‘𝐴)) | 
| 28 |  | uncom 4158 | . . . . . . . . . . 11
⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴) | 
| 29 | 28 | difeq1i 4122 | . . . . . . . . . 10
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) | 
| 30 |  | difun2 4481 | . . . . . . . . . 10
⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴) | 
| 31 | 29, 30 | eqtri 2765 | . . . . . . . . 9
⊢ ((𝐴 ∪ 𝐵) ∖ 𝐴) = (𝐵 ∖ 𝐴) | 
| 32 | 21 | eqeq1i 2742 | . . . . . . . . . 10
⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅) | 
| 33 |  | disj3 4454 | . . . . . . . . . 10
⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴)) | 
| 34 | 32, 33 | sylbb1 237 | . . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) = ∅ → 𝐵 = (𝐵 ∖ 𝐴)) | 
| 35 | 31, 34 | eqtr4id 2796 | . . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) ∖ 𝐴) = 𝐵) | 
| 36 | 35 | fveq2d 6910 | . . . . . . 7
⊢ ((𝐴 ∩ 𝐵) = ∅ → (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴)) = (vol*‘𝐵)) | 
| 37 | 27, 36 | oveq12d 7449 | . . . . . 6
⊢ ((𝐴 ∩ 𝐵) = ∅ → ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴))) = ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 38 | 18, 37 | syl 17 | . . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → ((vol*‘((𝐴 ∪ 𝐵) ∩ 𝐴)) + (vol*‘((𝐴 ∪ 𝐵) ∖ 𝐴))) = ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 39 | 17, 38 | eqtrd 2777 | . . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ)) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵))) | 
| 40 | 39 | ex 412 | . . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol*‘𝐴) ∈ ℝ ∧
(vol*‘𝐵) ∈
ℝ) → (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) | 
| 41 |  | mblvol 25565 | . . . . . 6
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) | 
| 42 | 41 | eleq1d 2826 | . . . . 5
⊢ (𝐴 ∈ dom vol →
((vol‘𝐴) ∈
ℝ ↔ (vol*‘𝐴) ∈ ℝ)) | 
| 43 |  | mblvol 25565 | . . . . . 6
⊢ (𝐵 ∈ dom vol →
(vol‘𝐵) =
(vol*‘𝐵)) | 
| 44 | 43 | eleq1d 2826 | . . . . 5
⊢ (𝐵 ∈ dom vol →
((vol‘𝐵) ∈
ℝ ↔ (vol*‘𝐵) ∈ ℝ)) | 
| 45 | 42, 44 | bi2anan9 638 | . . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
(((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ) ↔ ((vol*‘𝐴) ∈ ℝ ∧ (vol*‘𝐵) ∈
ℝ))) | 
| 46 | 45 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ) ↔ ((vol*‘𝐴) ∈ ℝ ∧ (vol*‘𝐵) ∈
ℝ))) | 
| 47 |  | unmbl 25572 | . . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∪ 𝐵) ∈ dom vol) | 
| 48 |  | mblvol 25565 | . . . . . 6
⊢ ((𝐴 ∪ 𝐵) ∈ dom vol → (vol‘(𝐴 ∪ 𝐵)) = (vol*‘(𝐴 ∪ 𝐵))) | 
| 49 | 47, 48 | syl 17 | . . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
(vol‘(𝐴 ∪ 𝐵)) = (vol*‘(𝐴 ∪ 𝐵))) | 
| 50 | 41, 43 | oveqan12d 7450 | . . . . 5
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
((vol‘𝐴) +
(vol‘𝐵)) =
((vol*‘𝐴) +
(vol*‘𝐵))) | 
| 51 | 49, 50 | eqeq12d 2753 | . . . 4
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) →
((vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)) ↔ (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) | 
| 52 | 51 | 3adant3 1133 | . . 3
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → ((vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)) ↔ (vol*‘(𝐴 ∪ 𝐵)) = ((vol*‘𝐴) + (vol*‘𝐵)))) | 
| 53 | 40, 46, 52 | 3imtr4d 294 | . 2
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) → (((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵)))) | 
| 54 | 53 | imp 406 | 1
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ (𝐴 ∩ 𝐵) = ∅) ∧ ((vol‘𝐴) ∈ ℝ ∧
(vol‘𝐵) ∈
ℝ)) → (vol‘(𝐴 ∪ 𝐵)) = ((vol‘𝐴) + (vol‘𝐵))) |