Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 ismbl2 ${⊢}{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}\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 ¬{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 ffvelrni ${⊢}{x}\in 𝒫ℝ\to {vol}^{*}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]$
30 29 adantr ${⊢}\left({x}\in 𝒫ℝ\wedge ¬{vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]$
31 simpr ${⊢}\left({x}\in 𝒫ℝ\wedge ¬{vol}^{*}\left({x}\right)\in ℝ\right)\to ¬{vol}^{*}\left({x}\right)\in ℝ$
32 xrge0nre ${⊢}\left({vol}^{*}\left({x}\right)\in \left[0,\mathrm{+\infty }\right]\wedge ¬{vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)=\mathrm{+\infty }$
33 30 31 32 syl2anc ${⊢}\left({x}\in 𝒫ℝ\wedge ¬{vol}^{*}\left({x}\right)\in ℝ\right)\to {vol}^{*}\left({x}\right)=\mathrm{+\infty }$
34 33 eqcomd ${⊢}\left({x}\in 𝒫ℝ\wedge ¬{vol}^{*}\left({x}\right)\in ℝ\right)\to \mathrm{+\infty }={vol}^{*}\left({x}\right)$
35 27 34 breqtrd ${⊢}\left({x}\in 𝒫ℝ\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)$
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 ¬{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)↔{vol}^{*}\left({x}\cap {A}\right){+}_{𝑒}{vol}^{*}\left({x}\setminus {A}\right)\le {vol}^{*}\left({x}\right)\right)$
45 44 ralbiia ${⊢}\forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}\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)↔\forall {x}\in 𝒫ℝ\phantom{\rule{.4em}{0ex}}{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 𝒫ℝ\phantom{\rule{.4em}{0ex}}\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)↔\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)$
47 1 46 bitri ${⊢}{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)$