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 φ X Fin
Assertion isvonmbl φ E dom voln X E X a 𝒫 X voln* X a E + 𝑒 voln* X a E = voln* X a

Proof

Step Hyp Ref Expression
1 isvonmbl.1 φ X Fin
2 1 dmvon φ dom voln X = CaraGen voln* X
3 2 eleq2d φ E dom voln X E CaraGen voln* X
4 1 ovnome φ voln* X OutMeas
5 eqid CaraGen voln* X = CaraGen voln* X
6 4 5 caragenel φ E CaraGen voln* X E 𝒫 dom voln* X a 𝒫 dom voln* X voln* X a E + 𝑒 voln* X a E = voln* X a
7 elpwi E 𝒫 dom voln* X E dom voln* X
8 7 adantl φ E 𝒫 dom voln* X E dom voln* X
9 1 unidmovn φ dom voln* X = X
10 9 adantr φ E 𝒫 dom voln* X dom voln* X = X
11 8 10 sseqtrd φ E 𝒫 dom voln* X E X
12 11 ex φ E 𝒫 dom voln* X E X
13 simpr φ E X E X
14 9 eqcomd φ X = dom voln* X
15 14 adantr φ E X X = dom voln* X
16 13 15 sseqtrd φ E X E dom voln* X
17 ovex X V
18 17 ssex E X E V
19 elpwg E V E 𝒫 dom voln* X E dom voln* X
20 18 19 syl E X E 𝒫 dom voln* X E dom voln* X
21 20 adantl φ E X E 𝒫 dom voln* X E dom voln* X
22 16 21 mpbird φ E X E 𝒫 dom voln* X
23 22 ex φ E X E 𝒫 dom voln* X
24 12 23 impbid φ E 𝒫 dom voln* X E X
25 9 pweqd φ 𝒫 dom voln* X = 𝒫 X
26 raleq 𝒫 dom voln* X = 𝒫 X a 𝒫 dom voln* X voln* X a E + 𝑒 voln* X a E = voln* X a a 𝒫 X voln* X a E + 𝑒 voln* X a E = voln* X a
27 25 26 syl φ a 𝒫 dom voln* X voln* X a E + 𝑒 voln* X a E = voln* X a a 𝒫 X voln* X a E + 𝑒 voln* X a E = voln* X a
28 24 27 anbi12d φ E 𝒫 dom voln* X a 𝒫 dom voln* X voln* X a E + 𝑒 voln* X a E = voln* X a E X a 𝒫 X voln* X a E + 𝑒 voln* X a E = voln* X a
29 3 6 28 3bitrd φ E dom voln X E X a 𝒫 X voln* X a E + 𝑒 voln* X a E = voln* X a