# Metamath Proof Explorer

## 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↔\left({A}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{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↔\left({A}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{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)↔{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right){+}_{𝑒}{vol}^{*}\left({x}\setminus {A}\right)\right)$
28 27 ralbiia ${⊢}\forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\cap {A}\right){+}_{𝑒}{vol}^{*}\left({x}\setminus {A}\right)\le {vol}^{*}\left({x}\right)↔\forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{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 𝒫ℝ\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\cap {A}\right){+}_{𝑒}{vol}^{*}\left({x}\setminus {A}\right)\le {vol}^{*}\left({x}\right)\right)↔\left({A}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{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↔\left({A}\subseteq ℝ\wedge \forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({x}\right)={vol}^{*}\left({x}\cap {A}\right){+}_{𝑒}{vol}^{*}\left({x}\setminus {A}\right)\right)$