# Metamath Proof Explorer

## Theorem mblsplit

Description: The defining property of measurability. (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion mblsplit ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)$

### Proof

Step Hyp Ref Expression
1 reex ${⊢}ℝ\in \mathrm{V}$
2 1 elpw2 ${⊢}{B}\in 𝒫ℝ↔{B}\subseteq ℝ$
3 ismbl ${⊢}{A}\in \mathrm{dom}vol↔\left({A}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}\left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)\right)$
4 fveq2 ${⊢}{x}={B}\to {vol}^{*}\left({x}\right)={vol}^{*}\left({B}\right)$
5 4 eleq1d ${⊢}{x}={B}\to \left({vol}^{*}\left({x}\right)\in ℝ↔{vol}^{*}\left({B}\right)\in ℝ\right)$
6 ineq1 ${⊢}{x}={B}\to {x}\cap {A}={B}\cap {A}$
7 6 fveq2d ${⊢}{x}={B}\to {vol}^{*}\left({x}\cap {A}\right)={vol}^{*}\left({B}\cap {A}\right)$
8 difeq1 ${⊢}{x}={B}\to {x}\setminus {A}={B}\setminus {A}$
9 8 fveq2d ${⊢}{x}={B}\to {vol}^{*}\left({x}\setminus {A}\right)={vol}^{*}\left({B}\setminus {A}\right)$
10 7 9 oveq12d ${⊢}{x}={B}\to {vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)$
11 4 10 eqeq12d ${⊢}{x}={B}\to \left({vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)↔{vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)\right)$
12 5 11 imbi12d ${⊢}{x}={B}\to \left(\left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)↔\left({vol}^{*}\left({B}\right)\in ℝ\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)\right)\right)$
13 12 rspccv ${⊢}\forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}\left({vol}^{*}\left({x}\right)\in ℝ\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)\to \left({B}\in 𝒫ℝ\to \left({vol}^{*}\left({B}\right)\in ℝ\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)\right)\right)$
14 3 13 simplbiim ${⊢}{A}\in \mathrm{dom}vol\to \left({B}\in 𝒫ℝ\to \left({vol}^{*}\left({B}\right)\in ℝ\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)\right)\right)$
15 2 14 syl5bir ${⊢}{A}\in \mathrm{dom}vol\to \left({B}\subseteq ℝ\to \left({vol}^{*}\left({B}\right)\in ℝ\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)\right)\right)$
16 15 3imp ${⊢}\left({A}\in \mathrm{dom}vol\wedge {B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\to {vol}^{*}\left({B}\right)={vol}^{*}\left({B}\cap {A}\right)+{vol}^{*}\left({B}\setminus {A}\right)$