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 e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismbl3 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
2 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
3 ovolcl 
 |-  ( x C_ RR -> ( vol* ` x ) e. RR* )
4 2 3 syl 
 |-  ( x e. ~P RR -> ( vol* ` x ) e. RR* )
5 4 adantr 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( vol* ` x ) e. RR* )
6 inss1 
 |-  ( x i^i A ) C_ x
7 6 2 sstrid 
 |-  ( x e. ~P RR -> ( x i^i A ) C_ RR )
8 ovolcl 
 |-  ( ( x i^i A ) C_ RR -> ( vol* ` ( x i^i A ) ) e. RR* )
9 7 8 syl 
 |-  ( x e. ~P RR -> ( vol* ` ( x i^i A ) ) e. RR* )
10 2 ssdifssd 
 |-  ( x e. ~P RR -> ( x \ A ) C_ RR )
11 ovolcl 
 |-  ( ( x \ A ) C_ RR -> ( vol* ` ( x \ A ) ) e. RR* )
12 10 11 syl 
 |-  ( x e. ~P RR -> ( vol* ` ( x \ A ) ) e. RR* )
13 9 12 xaddcld 
 |-  ( x e. ~P RR -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) e. RR* )
14 13 adantr 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) e. RR* )
15 2 ovolsplit 
 |-  ( x e. ~P RR -> ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
16 15 adantr 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( vol* ` x ) <_ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
17 simpr 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
18 5 14 16 17 xrletrid 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
19 18 ex 
 |-  ( x e. ~P RR -> ( ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )
20 13 xrleidd 
 |-  ( x e. ~P RR -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
21 20 adantr 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
22 id 
 |-  ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) -> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
23 22 eqcomd 
 |-  ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) = ( vol* ` x ) )
24 23 adantl 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) = ( vol* ` x ) )
25 21 24 breqtrd 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
26 25 ex 
 |-  ( x e. ~P RR -> ( ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
27 19 26 impbid 
 |-  ( x e. ~P RR -> ( ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) <-> ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )
28 27 ralbiia 
 |-  ( A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) <-> A. x e. ~P RR ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
29 28 anbi2i 
 |-  ( ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) <-> ( A C_ RR /\ A. x e. ~P RR ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )
30 1 29 bitri 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( vol* ` x ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) ) )