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\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)$$

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)\leftrightarrow {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]{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap y\right)+{vol}^{*}\left(x\setminus y\right)\leftrightarrow \forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)$$
8		df-vol	$$⊢vol={{vol}^{*}\upharpoonright }_{\left\{y|\forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{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}^{*}\upharpoonright }_{\left\{y|\forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap y\right)+{vol}^{*}\left(x\setminus y\right)\right\}}\right)$$
10		dmres	$$⊢\mathrm{dom}\left({{vol}^{*}\upharpoonright }_{\left\{y|\forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{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]{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]{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]{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]{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]{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]{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]{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\leftrightarrow \left(A\in 𝒫ℝ\wedge \forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{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 𝒫ℝ\leftrightarrow 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]\leftrightarrow \left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)$$
22	11 20 21	mp2b	$$⊢x\in {{vol}^{*}}^{-1}\left[ℝ\right]\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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)\leftrightarrow \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]{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\leftrightarrow \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)$$
27	19 26	anbi12i	$$⊢\left(A\in 𝒫ℝ\wedge \forall x\in {{vol}^{*}}^{-1}\left[ℝ\right]{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\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)$$
28	17 27	bitri	$$⊢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)$$