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

Metamath Proof Explorer

Theorem ismbl

Description: The predicate " A is Lebesgue-measurable". A set is measurable if it splits every other set x in a "nice" way, that is, if the measure of the pieces x i^i A and x \ A sum up to the measure of x (assuming that the measure of x is a real number, so that this addition makes sense). (Contributed by Mario Carneiro, 17-Mar-2014)

Ref Expression
Assertion ismbl ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ineq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ 𝐴 ) )
2 1 fveq2d ⊢ ( 𝑦 = 𝐴 → ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) = ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) )
3 difeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑥 ∖ 𝑦 ) = ( 𝑥 ∖ 𝐴 ) )
4 3 fveq2d ⊢ ( 𝑦 = 𝐴 → ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) = ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) )
5 2 4 oveq12d ⊢ ( 𝑦 = 𝐴 → ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) )
6 5 eqeq2d ⊢ ( 𝑦 = 𝐴 → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) ↔ ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
7 6 ralbidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) ↔ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
8 df-vol ⊢ vol = ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } )
9 8 dmeqi ⊢ dom vol = dom ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } )
10 dmres ⊢ dom ( vol* ↾ { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ) = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ dom vol* )
11 ovolf ⊢ vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ )
12 11 fdmi ⊢ dom vol* = 𝒫 ℝ
13 12 ineq2i ⊢ ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ dom vol* ) = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
14 9 10 13 3eqtri ⊢ dom vol = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
15 dfrab2 ⊢ { 𝑦 ∈ 𝒫 ℝ ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } = ( { 𝑦 ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) } ∩ 𝒫 ℝ )
16 14 15 eqtr4i ⊢ dom vol = { 𝑦 ∈ 𝒫 ℝ ∣ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝑦 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝑦 ) ) ) }
17 7 16 elrab2 ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ∈ 𝒫 ℝ ∧ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
18 reex ⊢ ℝ ∈ V
19 18 elpw2 ⊢ ( 𝐴 ∈ 𝒫 ℝ ↔ 𝐴 ⊆ ℝ )
20 ffn ⊢ ( vol* : 𝒫 ℝ ⟶ ( 0 [,] +∞ ) → vol* Fn 𝒫 ℝ )
21 elpreima ⊢ ( vol* Fn 𝒫 ℝ → ( 𝑥 ∈ ( ◡ vol* “ ℝ ) ↔ ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) )
22 11 20 21 mp2b ⊢ ( 𝑥 ∈ ( ◡ vol* “ ℝ ) ↔ ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) )
23 22 imbi1i ⊢ ( ( 𝑥 ∈ ( ◡ vol* “ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
24 impexp ⊢ ( ( ( 𝑥 ∈ 𝒫 ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
25 23 24 bitri ⊢ ( ( 𝑥 ∈ ( ◡ vol* “ ℝ ) → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝑥 ∈ 𝒫 ℝ → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
26 25 ralbii2 ⊢ ( ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) )
27 19 26 anbi12i ⊢ ( ( 𝐴 ∈ 𝒫 ℝ ∧ ∀ 𝑥 ∈ ( ◡ vol* “ ℝ ) ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )
28 17 27 bitri ⊢ ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥 ∩ 𝐴 ) ) + ( vol* ‘ ( 𝑥 ∖ 𝐴 ) ) ) ) ) )