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 Fin l x , y k x if k = l −∞ y
hspmbllem3.x φ X Fin
hspmbllem3.i φ K X
hspmbllem3.y φ Y
hspmbllem3.a φ voln* X A
hspmbllem3.s φ A X
hspmbllem3.c C = a 𝒫 X l 2 X | a j k X . l j k
hspmbllem3.l L = h 2 X k X vol . h k
hspmbllem3.d D = a 𝒫 X r + i C a | sum^ j L i j voln* X a + 𝑒 r
hspmbllem3.10 B = j k X 1 st i j k
hspmbllem3.11 T = j k X 2 nd i j k
Assertion hspmbllem3 φ voln* X A K H X Y + 𝑒 voln* X A K H X Y voln* X A

Proof

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