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 𝒫ℝ\leftrightarrow B\subseteq ℝ$$
3		ismbl	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\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 ℝ\leftrightarrow {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)\leftrightarrow {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)\leftrightarrow \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 𝒫ℝ\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	biimtrrid	$$⊢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)$$