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 
|- ( ph -> X e. Fin )
Assertion isvonmbl 
|- ( ph -> ( E e. dom ( voln ` X ) <-> ( E C_ ( RR ^m X ) /\ A. a e. ~P ( RR ^m X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) ) )

Proof

Step Hyp Ref Expression
1 isvonmbl.1 
 |-  ( ph -> X e. Fin )
2 1 dmvon 
 |-  ( ph -> dom ( voln ` X ) = ( CaraGen ` ( voln* ` X ) ) )
3 2 eleq2d 
 |-  ( ph -> ( E e. dom ( voln ` X ) <-> E e. ( CaraGen ` ( voln* ` X ) ) ) )
4 1 ovnome 
 |-  ( ph -> ( voln* ` X ) e. OutMeas )
5 eqid 
 |-  ( CaraGen ` ( voln* ` X ) ) = ( CaraGen ` ( voln* ` X ) )
6 4 5 caragenel 
 |-  ( ph -> ( E e. ( CaraGen ` ( voln* ` X ) ) <-> ( E e. ~P U. dom ( voln* ` X ) /\ A. a e. ~P U. dom ( voln* ` X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) ) )
7 elpwi 
 |-  ( E e. ~P U. dom ( voln* ` X ) -> E C_ U. dom ( voln* ` X ) )
8 7 adantl 
 |-  ( ( ph /\ E e. ~P U. dom ( voln* ` X ) ) -> E C_ U. dom ( voln* ` X ) )
9 1 unidmovn 
 |-  ( ph -> U. dom ( voln* ` X ) = ( RR ^m X ) )
10 9 adantr 
 |-  ( ( ph /\ E e. ~P U. dom ( voln* ` X ) ) -> U. dom ( voln* ` X ) = ( RR ^m X ) )
11 8 10 sseqtrd 
 |-  ( ( ph /\ E e. ~P U. dom ( voln* ` X ) ) -> E C_ ( RR ^m X ) )
12 11 ex 
 |-  ( ph -> ( E e. ~P U. dom ( voln* ` X ) -> E C_ ( RR ^m X ) ) )
13 simpr 
 |-  ( ( ph /\ E C_ ( RR ^m X ) ) -> E C_ ( RR ^m X ) )
14 9 eqcomd 
 |-  ( ph -> ( RR ^m X ) = U. dom ( voln* ` X ) )
15 14 adantr 
 |-  ( ( ph /\ E C_ ( RR ^m X ) ) -> ( RR ^m X ) = U. dom ( voln* ` X ) )
16 13 15 sseqtrd 
 |-  ( ( ph /\ E C_ ( RR ^m X ) ) -> E C_ U. dom ( voln* ` X ) )
17 ovex 
 |-  ( RR ^m X ) e. _V
18 17 ssex 
 |-  ( E C_ ( RR ^m X ) -> E e. _V )
19 elpwg 
 |-  ( E e. _V -> ( E e. ~P U. dom ( voln* ` X ) <-> E C_ U. dom ( voln* ` X ) ) )
20 18 19 syl 
 |-  ( E C_ ( RR ^m X ) -> ( E e. ~P U. dom ( voln* ` X ) <-> E C_ U. dom ( voln* ` X ) ) )
21 20 adantl 
 |-  ( ( ph /\ E C_ ( RR ^m X ) ) -> ( E e. ~P U. dom ( voln* ` X ) <-> E C_ U. dom ( voln* ` X ) ) )
22 16 21 mpbird 
 |-  ( ( ph /\ E C_ ( RR ^m X ) ) -> E e. ~P U. dom ( voln* ` X ) )
23 22 ex 
 |-  ( ph -> ( E C_ ( RR ^m X ) -> E e. ~P U. dom ( voln* ` X ) ) )
24 12 23 impbid 
 |-  ( ph -> ( E e. ~P U. dom ( voln* ` X ) <-> E C_ ( RR ^m X ) ) )
25 9 pweqd 
 |-  ( ph -> ~P U. dom ( voln* ` X ) = ~P ( RR ^m X ) )
26 raleq 
 |-  ( ~P U. dom ( voln* ` X ) = ~P ( RR ^m X ) -> ( A. a e. ~P U. dom ( voln* ` X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) <-> A. a e. ~P ( RR ^m X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) )
27 25 26 syl 
 |-  ( ph -> ( A. a e. ~P U. dom ( voln* ` X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) <-> A. a e. ~P ( RR ^m X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) )
28 24 27 anbi12d 
 |-  ( ph -> ( ( E e. ~P U. dom ( voln* ` X ) /\ A. a e. ~P U. dom ( voln* ` X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) <-> ( E C_ ( RR ^m X ) /\ A. a e. ~P ( RR ^m X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) ) )
29 3 6 28 3bitrd 
 |-  ( ph -> ( E e. dom ( voln ` X ) <-> ( E C_ ( RR ^m X ) /\ A. a e. ~P ( RR ^m X ) ( ( ( voln* ` X ) ` ( a i^i E ) ) +e ( ( voln* ` X ) ` ( a \ E ) ) ) = ( ( voln* ` X ) ` a ) ) ) )