This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrrid ⊢ ( 𝐴 ∈ dom vol → ( 𝐵 ⊆ ℝ → ( ( vol* ‘ 𝐵 ) ∈ ℝ → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) ) )
16 15 3imp ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( vol* ‘ 𝐵 ) = ( ( vol* ‘ ( 𝐵 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝐵 ∖ 𝐴 ) ) ) )