Theorem ismbl3

Description: The predicate " A is Lebesgue-measurable". Similar to ismbl2 , 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	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)$$

Proof

Step	Hyp	Ref	Expression
1		ismbl2	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
2		inss1	$$⊢x\cap A\subseteq x$$
3	2	a1i	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\cap A\subseteq x$$
4		elpwi	$$⊢x\in 𝒫ℝ\to x\subseteq ℝ$$
5	4	adantr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\subseteq ℝ$$
6		simpr	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)\in ℝ$$
7		ovolsscl	$$⊢\left(x\cap A\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)\in ℝ$$
8	3 5 6 7	syl3anc	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)\in ℝ$$
9		difssd	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to x\setminus A\subseteq x$$
10		ovolsscl	$$⊢\left(x\setminus A\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus A\right)\in ℝ$$
11	9 5 6 10	syl3anc	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus A\right)\in ℝ$$
12	8 11	rexaddd	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)$$
13	12	adantlr	$$⊢\left(\left(x\in 𝒫ℝ\wedge \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)$$
14		id	$$⊢\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\to \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)$$
15	14	imp	$$⊢\left(\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
16	15	adantll	$$⊢\left(\left(x\in 𝒫ℝ\wedge \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
17	13 16	eqbrtrd	$$⊢\left(\left(x\in 𝒫ℝ\wedge \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
18	2 4	sstrid	$$⊢x\in 𝒫ℝ\to x\cap A\subseteq ℝ$$
19		ovolcl	$$⊢x\cap A\subseteq ℝ\to {vol}^{*}\left(x\cap A\right)\in {ℝ}^{*}$$
20	18 19	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right)\in {ℝ}^{*}$$
21	4	ssdifssd	$$⊢x\in 𝒫ℝ\to x\setminus A\subseteq ℝ$$
22		ovolcl	$$⊢x\setminus A\subseteq ℝ\to {vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
23	21 22	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
24	20 23	xaddcld	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}$$
25		pnfge	$$⊢{vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\in {ℝ}^{*}\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le \mathrm{+\infty }$$
26	24 25	syl	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le \mathrm{+\infty }$$
27	26	adantr	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le \mathrm{+\infty }$$
28		ovolf	$$⊢{vol}^{*}:𝒫ℝ⟶\left[0,\mathrm{+\infty }\right]$$
29	28	ffvelcdmi	$$⊢x\in 𝒫ℝ\to {vol}^{*}\left(x\right)\in \left[0,\mathrm{+\infty }\right]$$
30	29	adantr	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)\in \left[0,\mathrm{+\infty }\right]$$
31		simpr	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to \neg {vol}^{*}\left(x\right)\in ℝ$$
32		xrge0nre	$$⊢\left({vol}^{*}\left(x\right)\in \left[0,\mathrm{+\infty }\right]\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)=\mathrm{+\infty }$$
33	30 31 32	syl2anc	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\right)=\mathrm{+\infty }$$
34	33	eqcomd	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to \mathrm{+\infty }={vol}^{*}\left(x\right)$$
35	27 34	breqtrd	$$⊢\left(x\in 𝒫ℝ\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
36	35	adantlr	$$⊢\left(\left(x\in 𝒫ℝ\wedge \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\wedge \neg {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
37	17 36	pm2.61dan	$$⊢\left(x\in 𝒫ℝ\wedge \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
38	37	ex	$$⊢x\in 𝒫ℝ\to \left(\left({vol}^{*}\left(x\right)\in ℝ\to {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)\right)$$
39	12	eqcomd	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
40	39	3adant2	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)={vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)$$
41		simp2	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
42	40 41	eqbrtrd	$$⊢\left(x\in 𝒫ℝ\wedge {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
43	42	3exp	$$⊢x\in 𝒫ℝ\to \left({vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\to \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
44	38 43	impbid	$$⊢x\in 𝒫ℝ\to \left(\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\leftrightarrow {vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)$$
45	44	ralbiia	$$⊢\forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\leftrightarrow \forall x\in 𝒫ℝ{vol}^{*}\left(x\cap A\right){+}_{𝑒}{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)$$
46	45	anbi2i	$$⊢\left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)\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)$$
47	1 46	bitri	$$⊢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)$$