Proof of Theorem volinun
| Step | Hyp | Ref
| Expression |
| 1 | | inundif 4479 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴 |
| 2 | 1 | fveq2i 6909 |
. . . 4
⊢
(vol‘((𝐴 ∩
𝐵) ∪ (𝐴 ∖ 𝐵))) = (vol‘𝐴) |
| 3 | | inmbl 25577 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∩ 𝐵) ∈ dom vol) |
| 4 | 3 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ∈ dom
vol) |
| 5 | | difmbl 25578 |
. . . . . 6
⊢ ((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) → (𝐴 ∖ 𝐵) ∈ dom vol) |
| 6 | 5 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ∈ dom
vol) |
| 7 | | indifcom 4283 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) |
| 8 | | difin0 4474 |
. . . . . . . . 9
⊢ ((𝐴 ∩ 𝐵) ∖ 𝐵) = ∅ |
| 9 | 8 | ineq2i 4217 |
. . . . . . . 8
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = (𝐴 ∩ ∅) |
| 10 | | in0 4395 |
. . . . . . . 8
⊢ (𝐴 ∩ ∅) =
∅ |
| 11 | 9, 10 | eqtri 2765 |
. . . . . . 7
⊢ (𝐴 ∩ ((𝐴 ∩ 𝐵) ∖ 𝐵)) = ∅ |
| 12 | 7, 11 | eqtri 2765 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅ |
| 13 | 12 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) |
| 14 | | mblvol 25565 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ dom vol → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
| 15 | 4, 14 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) = (vol*‘(𝐴 ∩ 𝐵))) |
| 16 | | inss1 4237 |
. . . . . . . 8
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 17 | 16 | a1i 11 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∩ 𝐵) ⊆ 𝐴) |
| 18 | | mblss 25566 |
. . . . . . . 8
⊢ (𝐴 ∈ dom vol → 𝐴 ⊆
ℝ) |
| 19 | 18 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐴
⊆ ℝ) |
| 20 | | mblvol 25565 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom vol →
(vol‘𝐴) =
(vol*‘𝐴)) |
| 21 | 20 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = (vol*‘𝐴)) |
| 22 | | simprl 771 |
. . . . . . . 8
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) ∈ ℝ) |
| 23 | 21, 22 | eqeltrrd 2842 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘𝐴) ∈ ℝ) |
| 24 | | ovolsscl 25521 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∩ 𝐵)) ∈
ℝ) |
| 25 | 17, 19, 23, 24 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
| 26 | 15, 25 | eqeltrd 2841 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℝ) |
| 27 | | mblvol 25565 |
. . . . . . 7
⊢ ((𝐴 ∖ 𝐵) ∈ dom vol → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
| 28 | 6, 27 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) = (vol*‘(𝐴 ∖ 𝐵))) |
| 29 | | difssd 4137 |
. . . . . . 7
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (𝐴
∖ 𝐵) ⊆ 𝐴) |
| 30 | | ovolsscl 25521 |
. . . . . . 7
⊢ (((𝐴 ∖ 𝐵) ⊆ 𝐴 ∧ 𝐴 ⊆ ℝ ∧ (vol*‘𝐴) ∈ ℝ) →
(vol*‘(𝐴 ∖
𝐵)) ∈
ℝ) |
| 31 | 29, 19, 23, 30 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol*‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
| 32 | 28, 31 | eqeltrd 2841 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ) |
| 33 | | volun 25580 |
. . . . 5
⊢ ((((𝐴 ∩ 𝐵) ∈ dom vol ∧ (𝐴 ∖ 𝐵) ∈ dom vol ∧ ((𝐴 ∩ 𝐵) ∩ (𝐴 ∖ 𝐵)) = ∅) ∧ ((vol‘(𝐴 ∩ 𝐵)) ∈ ℝ ∧ (vol‘(𝐴 ∖ 𝐵)) ∈ ℝ)) →
(vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
| 34 | 4, 6, 13, 26, 32, 33 | syl32anc 1380 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
| 35 | 2, 34 | eqtr3id 2791 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐴) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵)))) |
| 36 | 35 | oveq1d 7446 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵))) |
| 37 | 26 | recnd 11289 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∩ 𝐵)) ∈ ℂ) |
| 38 | 32 | recnd 11289 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘(𝐴 ∖ 𝐵)) ∈ ℂ) |
| 39 | | simprr 773 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℝ) |
| 40 | 39 | recnd 11289 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘𝐵) ∈ ℂ) |
| 41 | 37, 38, 40 | addassd 11283 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∖ 𝐵))) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)))) |
| 42 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → 𝐵
∈ dom vol) |
| 43 | | disjdifr 4473 |
. . . . . 6
⊢ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅ |
| 44 | 43 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((𝐴
∖ 𝐵) ∩ 𝐵) = ∅) |
| 45 | | volun 25580 |
. . . . 5
⊢ ((((𝐴 ∖ 𝐵) ∈ dom vol ∧ 𝐵 ∈ dom vol ∧ ((𝐴 ∖ 𝐵) ∩ 𝐵) = ∅) ∧ ((vol‘(𝐴 ∖ 𝐵)) ∈ ℝ ∧ (vol‘𝐵) ∈ ℝ)) →
(vol‘((𝐴 ∖
𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
| 46 | 6, 42, 44, 32, 39, 45 | syl32anc 1380 |
. . . 4
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → (vol‘((𝐴 ∖ 𝐵) ∪ 𝐵)) = ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) |
| 47 | | undif1 4476 |
. . . . 5
⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵) |
| 48 | 47 | fveq2i 6909 |
. . . 4
⊢
(vol‘((𝐴
∖ 𝐵) ∪ 𝐵)) = (vol‘(𝐴 ∪ 𝐵)) |
| 49 | 46, 48 | eqtr3di 2792 |
. . 3
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵)) = (vol‘(𝐴 ∪ 𝐵))) |
| 50 | 49 | oveq2d 7447 |
. 2
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘(𝐴 ∩ 𝐵)) + ((vol‘(𝐴 ∖ 𝐵)) + (vol‘𝐵))) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |
| 51 | 36, 41, 50 | 3eqtrd 2781 |
1
⊢ (((𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol) ∧
((vol‘𝐴) ∈
ℝ ∧ (vol‘𝐵)
∈ ℝ)) → ((vol‘𝐴) + (vol‘𝐵)) = ((vol‘(𝐴 ∩ 𝐵)) + (vol‘(𝐴 ∪ 𝐵)))) |