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=xFinlx,ykxifk=l−∞y
hspmbllem3.x φXFin
hspmbllem3.i φKX
hspmbllem3.y φY
hspmbllem3.a φvoln*XA
hspmbllem3.s φAX
hspmbllem3.c C=a𝒫Xl2X|ajkX.ljk
hspmbllem3.l L=h2XkXvol.hk
hspmbllem3.d D=a𝒫Xr+iCa|sum^jLijvoln*Xa+𝑒r
hspmbllem3.10 B=jkX1stijk
hspmbllem3.11 T=jkX2ndijk
Assertion hspmbllem3 φvoln*XAKHXY+𝑒voln*XAKHXYvoln*XA

Proof

Step Hyp Ref Expression
1 hspmbllem3.h H=xFinlx,ykxifk=l−∞y
2 hspmbllem3.x φXFin
3 hspmbllem3.i φKX
4 hspmbllem3.y φY
5 hspmbllem3.a φvoln*XA
6 hspmbllem3.s φAX
7 hspmbllem3.c C=a𝒫Xl2X|ajkX.ljk
8 hspmbllem3.l L=h2XkXvol.hk
9 hspmbllem3.d D=a𝒫Xr+iCa|sum^jLijvoln*Xa+𝑒r
10 hspmbllem3.10 B=jkX1stijk
11 hspmbllem3.11 T=jkX2ndijk
12 inss1 AKHXYA
13 12 6 sstrid φAKHXYX
14 2 13 ovncl φvoln*XAKHXY0+∞
15 12 a1i φAKHXYA
16 2 15 6 ovnssle φvoln*XAKHXYvoln*XA
17 5 14 16 ge0lere φvoln*XAKHXY
18 6 ssdifssd φAKHXYX
19 2 18 ovncl φvoln*XAKHXY0+∞
20 difssd φAKHXYA
21 2 20 6 ovnssle φvoln*XAKHXYvoln*XA
22 5 19 21 ge0lere φvoln*XAKHXY
23 rexadd voln*XAKHXYvoln*XAKHXYvoln*XAKHXY+𝑒voln*XAKHXY=voln*XAKHXY+voln*XAKHXY
24 17 22 23 syl2anc φvoln*XAKHXY+𝑒voln*XAKHXY=voln*XAKHXY+voln*XAKHXY
25 2 adantr φe+XFin
26 3 ne0d φX
27 26 adantr φe+X
28 6 adantr φe+AX
29 simpr φe+e+
30 25 27 28 29 7 8 9 ovncvrrp φe+iiDAe
31 25 adantr φe+iDAeXFin
32 3 ad2antrr φe+iDAeKX
33 4 ad2antrr φe+iDAeY
34 29 adantr φe+iDAee+
35 28 adantr φe+iDAeAX
36 fveq1 i=hij=hj
37 36 fveq2d i=hLij=Lhj
38 37 mpteq2dv i=hjLij=jLhj
39 38 fveq2d i=hsum^jLij=sum^jLhj
40 39 breq1d i=hsum^jLijvoln*Xa+𝑒rsum^jLhjvoln*Xa+𝑒r
41 40 cbvrabv iCa|sum^jLijvoln*Xa+𝑒r=hCa|sum^jLhjvoln*Xa+𝑒r
42 41 mpteq2i r+iCa|sum^jLijvoln*Xa+𝑒r=r+hCa|sum^jLhjvoln*Xa+𝑒r
43 42 mpteq2i a𝒫Xr+iCa|sum^jLijvoln*Xa+𝑒r=a𝒫Xr+hCa|sum^jLhjvoln*Xa+𝑒r
44 9 43 eqtri D=a𝒫Xr+hCa|sum^jLhjvoln*Xa+𝑒r
45 simpr φe+iDAeiDAe
46 31 35 34 7 8 44 45 10 11 ovncvr2 φe+iDAeB:XT:XAjkXBjkTjksum^jkXvolBjkTjkvoln*XA+𝑒e
47 46 simplld φe+iDAeB:XT:X
48 47 simpld φe+iDAeB:X
49 47 simprd φe+iDAeT:X
50 46 simplrd φe+iDAeAjkXBjkTjk
51 46 simprd φe+iDAesum^jkXvolBjkTjkvoln*XA+𝑒e
52 5 adantr φe+voln*XA
53 29 rpred φe+e
54 52 53 rexaddd φe+voln*XA+𝑒e=voln*XA+e
55 54 adantr φe+iDAevoln*XA+𝑒e=voln*XA+e
56 51 55 breqtrd φe+iDAesum^jkXvolBjkTjkvoln*XA+e
57 5 ad2antrr φe+iDAevoln*XA
58 17 ad2antrr φe+iDAevoln*XAKHXY
59 22 ad2antrr φe+iDAevoln*XAKHXY
60 eqid xFinax,bxifx=0kxvolakbk=xFinax,bxifx=0kxvolakbk
61 eqid ycXhXifhXKchifchychy=ycXhXifhXKchifchychy
62 eqid xcXhXifh=Kifxchchxch=xcXhXifh=Kifxchchxch
63 1 31 32 33 34 48 49 50 56 57 58 59 60 61 62 hspmbllem2 φe+iDAevoln*XAKHXY+voln*XAKHXYvoln*XA+e
64 63 ex φe+iDAevoln*XAKHXY+voln*XAKHXYvoln*XA+e
65 64 exlimdv φe+iiDAevoln*XAKHXY+voln*XAKHXYvoln*XA+e
66 30 65 mpd φe+voln*XAKHXY+voln*XAKHXYvoln*XA+e
67 66 ralrimiva φe+voln*XAKHXY+voln*XAKHXYvoln*XA+e
68 17 22 readdcld φvoln*XAKHXY+voln*XAKHXY
69 alrple voln*XAKHXY+voln*XAKHXYvoln*XAvoln*XAKHXY+voln*XAKHXYvoln*XAe+voln*XAKHXY+voln*XAKHXYvoln*XA+e
70 68 5 69 syl2anc φvoln*XAKHXY+voln*XAKHXYvoln*XAe+voln*XAKHXY+voln*XAKHXYvoln*XA+e
71 67 70 mpbird φvoln*XAKHXY+voln*XAKHXYvoln*XA
72 24 71 eqbrtrd φvoln*XAKHXY+𝑒voln*XAKHXYvoln*XA