Metamath Proof Explorer


Theorem isvonmbl

Description: The predicate " A is measurable w.r.t. the n-dimensional Lebesgue measure". 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 . Definition 114E of Fremlin1 p. 25. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypothesis isvonmbl.1 φXFin
Assertion isvonmbl φEdomvolnXEXa𝒫Xvoln*XaE+𝑒voln*XaE=voln*Xa

Proof

Step Hyp Ref Expression
1 isvonmbl.1 φXFin
2 1 dmvon φdomvolnX=CaraGenvoln*X
3 2 eleq2d φEdomvolnXECaraGenvoln*X
4 1 ovnome φvoln*XOutMeas
5 eqid CaraGenvoln*X=CaraGenvoln*X
6 4 5 caragenel φECaraGenvoln*XE𝒫domvoln*Xa𝒫domvoln*Xvoln*XaE+𝑒voln*XaE=voln*Xa
7 elpwi E𝒫domvoln*XEdomvoln*X
8 7 adantl φE𝒫domvoln*XEdomvoln*X
9 1 unidmovn φdomvoln*X=X
10 9 adantr φE𝒫domvoln*Xdomvoln*X=X
11 8 10 sseqtrd φE𝒫domvoln*XEX
12 11 ex φE𝒫domvoln*XEX
13 simpr φEXEX
14 9 eqcomd φX=domvoln*X
15 14 adantr φEXX=domvoln*X
16 13 15 sseqtrd φEXEdomvoln*X
17 ovex XV
18 17 ssex EXEV
19 elpwg EVE𝒫domvoln*XEdomvoln*X
20 18 19 syl EXE𝒫domvoln*XEdomvoln*X
21 20 adantl φEXE𝒫domvoln*XEdomvoln*X
22 16 21 mpbird φEXE𝒫domvoln*X
23 22 ex φEXE𝒫domvoln*X
24 12 23 impbid φE𝒫domvoln*XEX
25 9 pweqd φ𝒫domvoln*X=𝒫X
26 raleq 𝒫domvoln*X=𝒫Xa𝒫domvoln*Xvoln*XaE+𝑒voln*XaE=voln*Xaa𝒫Xvoln*XaE+𝑒voln*XaE=voln*Xa
27 25 26 syl φa𝒫domvoln*Xvoln*XaE+𝑒voln*XaE=voln*Xaa𝒫Xvoln*XaE+𝑒voln*XaE=voln*Xa
28 24 27 anbi12d φE𝒫domvoln*Xa𝒫domvoln*Xvoln*XaE+𝑒voln*XaE=voln*XaEXa𝒫Xvoln*XaE+𝑒voln*XaE=voln*Xa
29 3 6 28 3bitrd φEdomvolnXEXa𝒫Xvoln*XaE+𝑒voln*XaE=voln*Xa