# 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 ${⊢}{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)$

### Proof

Step Hyp Ref Expression
1 ineq2 ${⊢}{y}={A}\to {x}\cap {y}={x}\cap {A}$
2 1 fveq2d ${⊢}{y}={A}\to {vol}^{*}\left({x}\cap {y}\right)={vol}^{*}\left({x}\cap {A}\right)$
3 difeq2 ${⊢}{y}={A}\to {x}\setminus {y}={x}\setminus {A}$
4 3 fveq2d ${⊢}{y}={A}\to {vol}^{*}\left({x}\setminus {y}\right)={vol}^{*}\left({x}\setminus {A}\right)$
5 2 4 oveq12d ${⊢}{y}={A}\to {vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)$
6 5 eqeq2d ${⊢}{y}={A}\to \left({vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)↔{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)$
7 6 ralbidv ${⊢}{y}={A}\to \left(\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)↔\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)$
8 df-vol ${⊢}vol={{vol}^{*}↾}_{\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}}$
9 8 dmeqi ${⊢}\mathrm{dom}vol=\mathrm{dom}\left({{vol}^{*}↾}_{\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}}\right)$
10 dmres ${⊢}\mathrm{dom}\left({{vol}^{*}↾}_{\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}}\right)=\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}\cap \mathrm{dom}{vol}^{*}$
11 ovolf ${⊢}{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]$
12 11 fdmi ${⊢}\mathrm{dom}{vol}^{*}=𝒫ℝ$
13 12 ineq2i ${⊢}\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}\cap \mathrm{dom}{vol}^{*}=\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}\cap 𝒫ℝ$
14 9 10 13 3eqtri ${⊢}\mathrm{dom}vol=\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}\cap 𝒫ℝ$
15 dfrab2 ${⊢}\left\{{y}\in 𝒫ℝ|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}=\left\{{y}|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}\cap 𝒫ℝ$
16 14 15 eqtr4i ${⊢}\mathrm{dom}vol=\left\{{y}\in 𝒫ℝ|\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {y}\right)+{vol}^{*}\left({x}\setminus {y}\right)\right\}$
17 7 16 elrab2 ${⊢}{A}\in \mathrm{dom}vol↔\left({A}\in 𝒫ℝ\wedge \forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)$
18 reex ${⊢}ℝ\in \mathrm{V}$
19 18 elpw2 ${⊢}{A}\in 𝒫ℝ↔{A}\subseteq ℝ$
20 ffn ${⊢}{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]\to {vol}^{*}Fn𝒫ℝ$
21 elpreima ${⊢}{vol}^{*}Fn𝒫ℝ\to \left({x}\in {{vol}^{*}}^{-1}\left[ℝ\right]↔\left({x}\in 𝒫ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\right)$
22 11 20 21 mp2b ${⊢}{x}\in {{vol}^{*}}^{-1}\left[ℝ\right]↔\left({x}\in 𝒫ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)$
23 22 imbi1i ${⊢}\left({x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)↔\left(\left({x}\in 𝒫ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)$
24 impexp ${⊢}\left(\left({x}\in 𝒫ℝ\wedge {vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)↔\left({x}\in 𝒫ℝ\to \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)$
25 23 24 bitri ${⊢}\left({x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\to {vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)↔\left({x}\in 𝒫ℝ\to \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)$
26 25 ralbii2 ${⊢}\forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)↔\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)$
27 19 26 anbi12i ${⊢}\left({A}\in 𝒫ℝ\wedge \forall {x}\in {{vol}^{*}}^{-1}\left[ℝ\right]\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right)+{vol}^{*}\left({x}\setminus {A}\right)\right)↔\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)$
28 17 27 bitri ${⊢}{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)$