Metamath Proof Explorer

Theorem hspmbllem3

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. This proof handles the non-trivial cases (nonzero dimension and finite outer measure). (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbllem3.h 
|- H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
hspmbllem3.x 
|- ( ph -> X e. Fin )
hspmbllem3.i 
|- ( ph -> K e. X )
hspmbllem3.y 
|- ( ph -> Y e. RR )
hspmbllem3.a 
|- ( ph -> ( ( voln* ` X ) ` A ) e. RR )
hspmbllem3.s 
|- ( ph -> A C_ ( RR ^m X ) )
hspmbllem3.c 
|- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
hspmbllem3.l 
|- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
hspmbllem3.d 
|- D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
hspmbllem3.10 
|- B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( i ` j ) ` k ) ) ) )
hspmbllem3.11 
|- T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( i ` j ) ` k ) ) ) )
Assertion hspmbllem3 
|- ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` A ) )

Proof

Step Hyp Ref Expression
1 hspmbllem3.h 
 |-  H = ( x e. Fin |-> ( l e. x , y e. RR |-> X_ k e. x if ( k = l , ( -oo (,) y ) , RR ) ) )
2 hspmbllem3.x 
 |-  ( ph -> X e. Fin )
3 hspmbllem3.i 
 |-  ( ph -> K e. X )
4 hspmbllem3.y 
 |-  ( ph -> Y e. RR )
5 hspmbllem3.a 
 |-  ( ph -> ( ( voln* ` X ) ` A ) e. RR )
6 hspmbllem3.s 
 |-  ( ph -> A C_ ( RR ^m X ) )
7 hspmbllem3.c 
 |-  C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
8 hspmbllem3.l 
 |-  L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
9 hspmbllem3.d 
 |-  D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
10 hspmbllem3.10 
 |-  B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( i ` j ) ` k ) ) ) )
11 hspmbllem3.11 
 |-  T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( i ` j ) ` k ) ) ) )
12 inss1 
 |-  ( A i^i ( K ( H ` X ) Y ) ) C_ A
13 12 6 sstrid 
 |-  ( ph -> ( A i^i ( K ( H ` X ) Y ) ) C_ ( RR ^m X ) )
14 2 13 ovncl 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. ( 0 [,] +oo ) )
15 12 a1i 
 |-  ( ph -> ( A i^i ( K ( H ` X ) Y ) ) C_ A )
16 2 15 6 ovnssle 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) <_ ( ( voln* ` X ) ` A ) )
17 5 14 16 ge0lere 
 |-  ( ph -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. RR )
18 6 ssdifssd 
 |-  ( ph -> ( A \ ( K ( H ` X ) Y ) ) C_ ( RR ^m X ) )
19 2 18 ovncl 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. ( 0 [,] +oo ) )
20 difssd 
 |-  ( ph -> ( A \ ( K ( H ` X ) Y ) ) C_ A )
21 2 20 6 ovnssle 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) <_ ( ( voln* ` X ) ` A ) )
22 5 19 21 ge0lere 
 |-  ( ph -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. RR )
23 rexadd 
 |-  ( ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. RR /\ ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. RR ) -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) = ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) )
24 17 22 23 syl2anc 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) = ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) )
25 2 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> X e. Fin )
26 3 ne0d 
 |-  ( ph -> X =/= (/) )
27 26 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> X =/= (/) )
28 6 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> A C_ ( RR ^m X ) )
29 simpr 
 |-  ( ( ph /\ e e. RR+ ) -> e e. RR+ )
30 25 27 28 29 7 8 9 ovncvrrp 
 |-  ( ( ph /\ e e. RR+ ) -> E. i i e. ( ( D ` A ) ` e ) )
31 25 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> X e. Fin )
32 3 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> K e. X )
33 4 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> Y e. RR )
34 29 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> e e. RR+ )
35 28 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> A C_ ( RR ^m X ) )
36 fveq1 
 |-  ( i = h -> ( i ` j ) = ( h ` j ) )
37 36 fveq2d 
 |-  ( i = h -> ( L ` ( i ` j ) ) = ( L ` ( h ` j ) ) )
38 37 mpteq2dv 
 |-  ( i = h -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> ( L ` ( h ` j ) ) ) )
39 38 fveq2d 
 |-  ( i = h -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) )
40 39 breq1d 
 |-  ( i = h -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) ) )
41 40 cbvrabv 
 |-  { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } = { h e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) }
42 41 mpteq2i 
 |-  ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) = ( r e. RR+ |-> { h e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } )
43 42 mpteq2i 
 |-  ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) ) = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { h e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
44 9 43 eqtri 
 |-  D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { h e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( h ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
45 simpr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> i e. ( ( D ` A ) ` e ) )
46 31 35 34 7 8 44 45 10 11 ovncvr2 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) /\ A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) /\ ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) ) )
47 46 simplld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) )
48 47 simpld 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> B : NN --> ( RR ^m X ) )
49 47 simprd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> T : NN --> ( RR ^m X ) )
50 46 simplrd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
51 46 simprd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e e ) )
52 5 adantr 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( voln* ` X ) ` A ) e. RR )
53 29 rpred 
 |-  ( ( ph /\ e e. RR+ ) -> e e. RR )
54 52 53 rexaddd 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( ( voln* ` X ) ` A ) +e e ) = ( ( ( voln* ` X ) ` A ) + e ) )
55 54 adantr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( ( voln* ` X ) ` A ) +e e ) = ( ( ( voln* ` X ) ` A ) + e ) )
56 51 55 breqtrd 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) )
57 5 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( voln* ` X ) ` A ) e. RR )
58 17 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) e. RR )
59 22 ad2antrr 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) e. RR )
60 eqid 
 |-  ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) ) = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
61 eqid 
 |-  ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) ) = ( y e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h e. ( X \ { K } ) , ( c ` h ) , if ( ( c ` h ) <_ y , ( c ` h ) , y ) ) ) ) )
62 eqid 
 |-  ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m X ) |-> ( h e. X |-> if ( h = K , if ( x <_ ( c ` h ) , ( c ` h ) , x ) , ( c ` h ) ) ) ) )
63 1 31 32 33 34 48 49 50 56 57 58 59 60 61 62 hspmbllem2 
 |-  ( ( ( ph /\ e e. RR+ ) /\ i e. ( ( D ` A ) ` e ) ) -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) )
64 63 ex 
 |-  ( ( ph /\ e e. RR+ ) -> ( i e. ( ( D ` A ) ` e ) -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) ) )
65 64 exlimdv 
 |-  ( ( ph /\ e e. RR+ ) -> ( E. i i e. ( ( D ` A ) ` e ) -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) ) )
66 30 65 mpd 
 |-  ( ( ph /\ e e. RR+ ) -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) )
67 66 ralrimiva 
 |-  ( ph -> A. e e. RR+ ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) )
68 17 22 readdcld 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) e. RR )
69 alrple 
 |-  ( ( ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) e. RR /\ ( ( voln* ` X ) ` A ) e. RR ) -> ( ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` A ) <-> A. e e. RR+ ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) ) )
70 68 5 69 syl2anc 
 |-  ( ph -> ( ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` A ) <-> A. e e. RR+ ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) + e ) ) )
71 67 70 mpbird 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) + ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` A ) )
72 24 71 eqbrtrd 
 |-  ( ph -> ( ( ( voln* ` X ) ` ( A i^i ( K ( H ` X ) Y ) ) ) +e ( ( voln* ` X ) ` ( A \ ( K ( H ` X ) Y ) ) ) ) <_ ( ( voln* ` X ) ` A ) )