Metamath Proof Explorer


Theorem hspmbl

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hspmbl.1 H = x Fin l x , y k x if k = l −∞ y
hspmbl.x φ X Fin
hspmbl.i φ K X
hspmbl.y φ Y
Assertion hspmbl φ K H X Y dom voln X

Proof

Step Hyp Ref Expression
1 hspmbl.1 H = x Fin l x , y k x if k = l −∞ y
2 hspmbl.x φ X Fin
3 hspmbl.i φ K X
4 hspmbl.y φ Y
5 2 ovnome φ voln* X OutMeas
6 eqid dom voln* X = dom voln* X
7 eqid CaraGen voln* X = CaraGen voln* X
8 ovex −∞ Y V
9 reex V
10 8 9 ifex if p = K −∞ Y V
11 10 ixpssmap p X if p = K −∞ Y p X if p = K −∞ Y X
12 iftrue p = K if p = K −∞ Y = −∞ Y
13 ioossre −∞ Y
14 13 a1i p = K −∞ Y
15 12 14 eqsstrd p = K if p = K −∞ Y
16 iffalse ¬ p = K if p = K −∞ Y =
17 ssid
18 17 a1i ¬ p = K
19 16 18 eqsstrd ¬ p = K if p = K −∞ Y
20 15 19 pm2.61i if p = K −∞ Y
21 20 rgenw p X if p = K −∞ Y
22 iunss p X if p = K −∞ Y p X if p = K −∞ Y
23 21 22 mpbir p X if p = K −∞ Y
24 mapss V p X if p = K −∞ Y p X if p = K −∞ Y X X
25 9 23 24 mp2an p X if p = K −∞ Y X X
26 11 25 sstri p X if p = K −∞ Y X
27 10 rgenw p X if p = K −∞ Y V
28 ixpexg p X if p = K −∞ Y V p X if p = K −∞ Y V
29 27 28 ax-mp p X if p = K −∞ Y V
30 elpwg p X if p = K −∞ Y V p X if p = K −∞ Y 𝒫 X p X if p = K −∞ Y X
31 29 30 ax-mp p X if p = K −∞ Y 𝒫 X p X if p = K −∞ Y X
32 26 31 mpbir p X if p = K −∞ Y 𝒫 X
33 32 a1i φ p X if p = K −∞ Y 𝒫 X
34 equid x = x
35 eqid =
36 equequ1 k = p k = l p = l
37 36 ifbid k = p if k = l −∞ y = if p = l −∞ y
38 37 cbvixpv k x if k = l −∞ y = p x if p = l −∞ y
39 34 35 38 mpoeq123i l x , y k x if k = l −∞ y = l x , y p x if p = l −∞ y
40 39 mpteq2i x Fin l x , y k x if k = l −∞ y = x Fin l x , y p x if p = l −∞ y
41 1 40 eqtri H = x Fin l x , y p x if p = l −∞ y
42 41 2 3 4 hspval φ K H X Y = p X if p = K −∞ Y
43 2 ovnf φ voln* X : 𝒫 X 0 +∞
44 43 fdmd φ dom voln* X = 𝒫 X
45 44 unieqd φ dom voln* X = 𝒫 X
46 unipw 𝒫 X = X
47 46 a1i φ 𝒫 X = X
48 45 47 eqtrd φ dom voln* X = X
49 48 pweqd φ 𝒫 dom voln* X = 𝒫 X
50 42 49 eleq12d φ K H X Y 𝒫 dom voln* X p X if p = K −∞ Y 𝒫 X
51 33 50 mpbird φ K H X Y 𝒫 dom voln* X
52 simpl φ a 𝒫 dom voln* X φ
53 simpr φ a 𝒫 dom voln* X a 𝒫 dom voln* X
54 52 49 syl φ a 𝒫 dom voln* X 𝒫 dom voln* X = 𝒫 X
55 53 54 eleqtrd φ a 𝒫 dom voln* X a 𝒫 X
56 2 adantr φ a 𝒫 X X Fin
57 inss1 a K H X Y a
58 57 a1i a 𝒫 X a K H X Y a
59 elpwi a 𝒫 X a X
60 58 59 sstrd a 𝒫 X a K H X Y X
61 60 adantl φ a 𝒫 X a K H X Y X
62 56 61 ovnxrcl φ a 𝒫 X voln* X a K H X Y *
63 59 adantl φ a 𝒫 X a X
64 63 ssdifssd φ a 𝒫 X a K H X Y X
65 56 64 ovnxrcl φ a 𝒫 X voln* X a K H X Y *
66 62 65 xaddcld φ a 𝒫 X voln* X a K H X Y + 𝑒 voln* X a K H X Y *
67 pnfge 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 +∞
68 66 67 syl φ a 𝒫 X voln* X a K H X Y + 𝑒 voln* X a K H X Y +∞
69 68 adantr φ a 𝒫 X voln* X a = +∞ voln* X a K H X Y + 𝑒 voln* X a K H X Y +∞
70 id voln* X a = +∞ voln* X a = +∞
71 70 eqcomd voln* X a = +∞ +∞ = voln* X a
72 71 adantl φ a 𝒫 X voln* X a = +∞ +∞ = voln* X a
73 69 72 breqtrd φ a 𝒫 X voln* X a = +∞ voln* X a K H X Y + 𝑒 voln* X a K H X Y voln* X a
74 simpl φ a 𝒫 X ¬ voln* X a = +∞ φ a 𝒫 X
75 56 63 ovncl φ a 𝒫 X voln* X a 0 +∞
76 75 adantr φ a 𝒫 X ¬ voln* X a = +∞ voln* X a 0 +∞
77 neqne ¬ voln* X a = +∞ voln* X a +∞
78 77 adantl φ a 𝒫 X ¬ voln* X a = +∞ voln* X a +∞
79 ge0xrre voln* X a 0 +∞ voln* X a +∞ voln* X a
80 76 78 79 syl2anc φ a 𝒫 X ¬ voln* X a = +∞ voln* X a
81 56 adantr φ a 𝒫 X voln* X a X Fin
82 3 ad2antrr φ a 𝒫 X voln* X a K X
83 4 ad2antrr φ a 𝒫 X voln* X a Y
84 simpr φ a 𝒫 X voln* X a voln* X a
85 63 adantr φ a 𝒫 X voln* X a a X
86 sseq1 a = b a j p X . l j p b j p X . l j p
87 86 rabbidv a = b l 2 X | a j p X . l j p = l 2 X | b j p X . l j p
88 87 cbvmptv a 𝒫 X l 2 X | a j p X . l j p = b 𝒫 X l 2 X | b j p X . l j p
89 simpl i = h p X i = h
90 89 coeq2d i = h p X . i = . h
91 90 fveq1d i = h p X . i p = . h p
92 91 fveq2d i = h p X vol . i p = vol . h p
93 92 prodeq2dv i = h p X vol . i p = p X vol . h p
94 93 cbvmptv i 2 X p X vol . i p = h 2 X p X vol . h p
95 fveq2 n = p . m i n = . m i p
96 95 cbvixpv n X . m i n = p X . m i p
97 96 a1i m = h n X . m i n = p X . m i p
98 fveq1 m = h m i = h i
99 98 coeq2d m = h . m i = . h i
100 99 fveq1d m = h . m i p = . h i p
101 100 ixpeq2dv m = h p X . m i p = p X . h i p
102 97 101 eqtrd m = h n X . m i n = p X . h i p
103 102 adantr m = h i n X . m i n = p X . h i p
104 103 iuneq2dv m = h i n X . m i n = i p X . h i p
105 104 sseq2d m = h a i n X . m i n a i p X . h i p
106 105 cbvrabv m 2 X | a i n X . m i n = h 2 X | a i p X . h i p
107 fveq1 h = l h i = l i
108 107 coeq2d h = l . h i = . l i
109 108 fveq1d h = l . h i p = . l i p
110 109 ixpeq2dv h = l p X . h i p = p X . l i p
111 110 adantr h = l i p X . h i p = p X . l i p
112 111 iuneq2dv h = l i p X . h i p = i p X . l i p
113 fveq2 i = j l i = l j
114 113 coeq2d i = j . l i = . l j
115 114 fveq1d i = j . l i p = . l j p
116 115 ixpeq2dv i = j p X . l i p = p X . l j p
117 116 cbviunv i p X . l i p = j p X . l j p
118 117 a1i h = l i p X . l i p = j p X . l j p
119 112 118 eqtrd h = l i p X . h i p = j p X . l j p
120 119 sseq2d h = l a i p X . h i p a j p X . l j p
121 120 cbvrabv h 2 X | a i p X . h i p = l 2 X | a j p X . l j p
122 106 121 eqtri m 2 X | a i n X . m i n = l 2 X | a j p X . l j p
123 122 mpteq2i a 𝒫 X m 2 X | a i n X . m i n = a 𝒫 X l 2 X | a j p X . l j p
124 123 a1i c = b a 𝒫 X m 2 X | a i n X . m i n = a 𝒫 X l 2 X | a j p X . l j p
125 id c = b c = b
126 124 125 fveq12d c = b a 𝒫 X m 2 X | a i n X . m i n c = a 𝒫 X l 2 X | a j p X . l j p b
127 126 eleq2d c = b t a 𝒫 X m 2 X | a i n X . m i n c t a 𝒫 X l 2 X | a j p X . l j p b
128 2fveq3 m = p vol . i m = vol . i p
129 128 cbvprodv m X vol . i m = p X vol . i p
130 129 mpteq2i i 2 X m X vol . i m = i 2 X p X vol . i p
131 130 a1i m = j i 2 X m X vol . i m = i 2 X p X vol . i p
132 fveq2 m = j t m = t j
133 131 132 fveq12d m = j i 2 X m X vol . i m t m = i 2 X p X vol . i p t j
134 133 cbvmptv m i 2 X m X vol . i m t m = j i 2 X p X vol . i p t j
135 134 a1i c = b m i 2 X m X vol . i m t m = j i 2 X p X vol . i p t j
136 135 fveq2d c = b sum^ m i 2 X m X vol . i m t m = sum^ j i 2 X p X vol . i p t j
137 fveq2 c = b voln* X c = voln* X b
138 137 oveq1d c = b voln* X c + 𝑒 s = voln* X b + 𝑒 s
139 136 138 breq12d c = b sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s
140 127 139 anbi12d c = b t a 𝒫 X m 2 X | a i n X . m i n c sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s t a 𝒫 X l 2 X | a j p X . l j p b sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s
141 140 rabbidva2 c = b t a 𝒫 X m 2 X | a i n X . m i n c | sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s = t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s
142 141 mpteq2dv c = b s + t a 𝒫 X m 2 X | a i n X . m i n c | sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s = s + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s
143 eqidd s = r a 𝒫 X l 2 X | a j p X . l j p b = a 𝒫 X l 2 X | a j p X . l j p b
144 143 eleq2d s = r t a 𝒫 X l 2 X | a j p X . l j p b t a 𝒫 X l 2 X | a j p X . l j p b
145 oveq2 s = r voln* X b + 𝑒 s = voln* X b + 𝑒 r
146 145 breq2d s = r sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
147 144 146 anbi12d s = r t a 𝒫 X l 2 X | a j p X . l j p b sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s t a 𝒫 X l 2 X | a j p X . l j p b sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
148 147 rabbidva2 s = r t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s = t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
149 148 cbvmptv s + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s = r + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
150 149 a1i c = b s + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 s = r + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
151 142 150 eqtrd c = b s + t a 𝒫 X m 2 X | a i n X . m i n c | sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s = r + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
152 151 cbvmptv c 𝒫 X s + t a 𝒫 X m 2 X | a i n X . m i n c | sum^ m i 2 X m X vol . i m t m voln* X c + 𝑒 s = b 𝒫 X r + t a 𝒫 X l 2 X | a j p X . l j p b | sum^ j i 2 X p X vol . i p t j voln* X b + 𝑒 r
153 2fveq3 m = p 1 st t j m = 1 st t j p
154 153 cbvmptv m X 1 st t j m = p X 1 st t j p
155 154 mpteq2i j m X 1 st t j m = j p X 1 st t j p
156 fveq2 i = j t i = t j
157 156 fveq1d i = j t i m = t j m
158 157 fveq2d i = j 2 nd t i m = 2 nd t j m
159 158 mpteq2dv i = j m X 2 nd t i m = m X 2 nd t j m
160 2fveq3 m = p 2 nd t j m = 2 nd t j p
161 160 cbvmptv m X 2 nd t j m = p X 2 nd t j p
162 161 a1i i = j m X 2 nd t j m = p X 2 nd t j p
163 159 162 eqtrd i = j m X 2 nd t i m = p X 2 nd t j p
164 163 cbvmptv i m X 2 nd t i m = j p X 2 nd t j p
165 41 81 82 83 84 85 88 94 152 155 164 hspmbllem3 φ a 𝒫 X voln* X a voln* X a K H X Y + 𝑒 voln* X a K H X Y voln* X a
166 74 80 165 syl2anc φ a 𝒫 X ¬ voln* X a = +∞ voln* X a K H X Y + 𝑒 voln* X a K H X Y voln* X a
167 73 166 pm2.61dan φ a 𝒫 X voln* X a K H X Y + 𝑒 voln* X a K H X Y voln* X a
168 52 55 167 syl2anc φ a 𝒫 dom voln* X voln* X a K H X Y + 𝑒 voln* X a K H X Y voln* X a
169 5 6 7 51 168 caragenel2d φ K H X Y CaraGen voln* X
170 2 dmvon φ dom voln X = CaraGen voln* X
171 170 eqcomd φ CaraGen voln* X = dom voln X
172 169 171 eleqtrd φ K H X Y dom voln X