Theorem ismbl4

Description: The predicate " A is Lebesgue-measurable". Similar to ismbl , but here +e is used, and the precondition ( vol*x ) e. RR can be dropped. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Assertion	ismbl4	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismbl3	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ{vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)$$
2		elpwi	$$⊢x\in 𝒫ℝ\to x\subseteq ℝ$$
3		ovolcl	$$⊢x\subseteq ℝ\to {vol}^{*}\left(x\right)\in {ℝ}^{*}$$
4	2 3	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\right)\in {ℝ}^{*}$$
5	4	adantr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to {vol}^{*}\left(x\right)\in {ℝ}^{*}$$
6		inss1	$$⊢x\cap A\subseteq x$$
7	6 2	sstrid	$$⊢x\in 𝒫ℝ\to x\cap A\subseteq ℝ$$
8		ovolcl	$$⊢x\cap A\subseteq ℝ\to {vol}^{*}\left(x\cap A\right)\in {ℝ}^{*}$$
9	7 8	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right)\in {ℝ}^{*}$$
10	2	ssdifssd	$$⊢x\in 𝒫ℝ\to x\setminus A\subseteq ℝ$$
11		ovolcl	$$⊢x\setminus A\subseteq ℝ\to {vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
12	10 11	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
13	9 12	xaddcld	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
14	13	adantr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
15	2	ovolsplit	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
16	15	adantr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to {vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
17		simpr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
18	5 14 16 17	xrletrid	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
19	18	ex	$$⊢x\in 𝒫ℝ\to \left({vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)$$
20	13	xrleidd	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
21	20	adantr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
22		id	$$⊢{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
23	22	eqcomd	$$⊢{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\right)$$
24	23	adantl	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\right)$$
25	21 24	breqtrd	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
26	25	ex	$$⊢x\in 𝒫ℝ\to \left({vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)$$
27	19 26	impbid	$$⊢x\in 𝒫ℝ\to \left({vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\leftrightarrow {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)$$
28	27	ralbiia	$$⊢\forall x\in 𝒫ℝ{vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\leftrightarrow \forall x\in 𝒫ℝ{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
29	28	anbi2i	$$⊢\left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ{vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)$$
30	1 29	bitri	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ{vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\right)$$