Theorem mblsplit

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

	Ref	Expression
Assertion	mblsplit	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		reex	⊢ ℝ ∈ V
2	1	elpw2	⊢ ( 𝐵 ∈ 𝒫 ℝ ↔ 𝐵 ⊆ ℝ )
3		ismbl	⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
4		fveq2	⊢ ( 𝑥 = 𝐵 → ( vol* ‘ 𝑥 ) = ( vol* ‘ 𝐵 ) )
5	4	eleq1d	⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ 𝑥 ) ∈ ℝ ↔ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
6		ineq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
7	6	fveq2d	⊢ ( 𝑥 = 𝐵 → ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) = ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) )
8		difeq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) )
9	8	fveq2d	⊢ ( 𝑥 = 𝐵 → ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) = ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) )
10	7 9	oveq12d	⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
11	4 10	eqeq12d	⊢ ( 𝑥 = 𝐵 → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) )
12	5 11	imbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) )
13	12	rspccv	⊢ ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) → ( 𝐵 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) )
14	3 13	simplbiim	⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) )
15	2 14	syl5bir	⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ⊆ ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) )
16	15	3imp	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) )