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

Proof

Step Hyp Ref Expression
1 ismbl2 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
2 inss1 
 |-  ( x i^i A ) C_ x
3 2 a1i 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( x i^i A ) C_ x )
4 elpwi 
 |-  ( x e. ~P RR -> x C_ RR )
5 4 adantr 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> x C_ RR )
6 simpr 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` x ) e. RR )
7 ovolsscl 
 |-  ( ( ( x i^i A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
8 3 5 6 7 syl3anc 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x i^i A ) ) e. RR )
9 difssd 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( x \ A ) C_ x )
10 ovolsscl 
 |-  ( ( ( x \ A ) C_ x /\ x C_ RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
11 9 5 6 10 syl3anc 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( vol* ` ( x \ A ) ) e. RR )
12 8 11 rexaddd 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
13 12 adantlr 
 |-  ( ( ( x e. ~P RR /\ ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) )
14 id 
 |-  ( ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
15 14 imp 
 |-  ( ( ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
16 15 adantll 
 |-  ( ( ( x e. ~P RR /\ ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
17 13 16 eqbrtrd 
 |-  ( ( ( x e. ~P RR /\ ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
18 2 4 sstrid 
 |-  ( x e. ~P RR -> ( x i^i A ) C_ RR )
19 ovolcl 
 |-  ( ( x i^i A ) C_ RR -> ( vol* ` ( x i^i A ) ) e. RR* )
20 18 19 syl 
 |-  ( x e. ~P RR -> ( vol* ` ( x i^i A ) ) e. RR* )
21 4 ssdifssd 
 |-  ( x e. ~P RR -> ( x \ A ) C_ RR )
22 ovolcl 
 |-  ( ( x \ A ) C_ RR -> ( vol* ` ( x \ A ) ) e. RR* )
23 21 22 syl 
 |-  ( x e. ~P RR -> ( vol* ` ( x \ A ) ) e. RR* )
24 20 23 xaddcld 
 |-  ( x e. ~P RR -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) e. RR* )
25 pnfge 
 |-  ( ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) e. RR* -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ +oo )
26 24 25 syl 
 |-  ( x e. ~P RR -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ +oo )
27 26 adantr 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ +oo )
28 ovolf 
 |-  vol* : ~P RR --> ( 0 [,] +oo )
29 28 ffvelcdmi 
 |-  ( x e. ~P RR -> ( vol* ` x ) e. ( 0 [,] +oo ) )
30 29 adantr 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> ( vol* ` x ) e. ( 0 [,] +oo ) )
31 simpr 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> -. ( vol* ` x ) e. RR )
32 xrge0nre 
 |-  ( ( ( vol* ` x ) e. ( 0 [,] +oo ) /\ -. ( vol* ` x ) e. RR ) -> ( vol* ` x ) = +oo )
33 30 31 32 syl2anc 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> ( vol* ` x ) = +oo )
34 33 eqcomd 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> +oo = ( vol* ` x ) )
35 27 34 breqtrd 
 |-  ( ( x e. ~P RR /\ -. ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
36 35 adantlr 
 |-  ( ( ( x e. ~P RR /\ ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) /\ -. ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
37 17 36 pm2.61dan 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
38 37 ex 
 |-  ( x e. ~P RR -> ( ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
39 12 eqcomd 
 |-  ( ( x e. ~P RR /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
40 39 3adant2 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) = ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) )
41 simp2 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
42 40 41 eqbrtrd 
 |-  ( ( x e. ~P RR /\ ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) /\ ( vol* ` x ) e. RR ) -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
43 42 3exp 
 |-  ( x e. ~P RR -> ( ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) -> ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) )
44 38 43 impbid 
 |-  ( x e. ~P RR -> ( ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) <-> ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
45 44 ralbiia 
 |-  ( A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) <-> A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) )
46 45 anbi2i 
 |-  ( ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` x ) e. RR -> ( ( vol* ` ( x i^i A ) ) + ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) ) <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )
47 1 46 bitri 
 |-  ( A e. dom vol <-> ( A C_ RR /\ A. x e. ~P RR ( ( vol* ` ( x i^i A ) ) +e ( vol* ` ( x \ A ) ) ) <_ ( vol* ` x ) ) )