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 \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
	hspmbllem3.x	$⊢ φ \to X \in Fin$
	hspmbllem3.i	$⊢ φ \to K \in X$
	hspmbllem3.y	$⊢ φ \to Y \in ℝ$
	hspmbllem3.a	$⊢ φ \to voln* (X) (A) \in ℝ$
	hspmbllem3.s	$⊢ φ \to A \subseteq ℝ^{X}$
	hspmbllem3.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
	hspmbllem3.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
	hspmbllem3.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
	hspmbllem3.10	$⊢ B = (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (i (j) (k))))$
	hspmbllem3.11	$⊢ T = (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (i (j) (k))))$
Assertion	hspmbllem3	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) +_{𝑒} voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A)$

Proof

Step	Hyp	Ref	Expression
1		hspmbllem3.h	$⊢ H = (x \in Fin ⟼ (l \in x, y \in ℝ ⟼ \underset{k \in x}{⨉} if (k = l, (−∞, y), ℝ)))$
2		hspmbllem3.x	$⊢ φ \to X \in Fin$
3		hspmbllem3.i	$⊢ φ \to K \in X$
4		hspmbllem3.y	$⊢ φ \to Y \in ℝ$
5		hspmbllem3.a	$⊢ φ \to voln* (X) (A) \in ℝ$
6		hspmbllem3.s	$⊢ φ \to A \subseteq ℝ^{X}$
7		hspmbllem3.c	$⊢ C = (a \in 𝒫 (ℝ^{X}) ⟼ \{l \in ({({ℝ^{2}}^{X})}^{ℕ}) \| a \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ l (j)) (k)\})$
8		hspmbllem3.l	$⊢ L = (h \in ({ℝ^{2}}^{X}) ⟼ \prod_{k \in X} vol (([.) \circ h) (k)))$
9		hspmbllem3.d	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
10		hspmbllem3.10	$⊢ B = (j \in ℕ ⟼ (k \in X ⟼ 1^{st} (i (j) (k))))$
11		hspmbllem3.11	$⊢ T = (j \in ℕ ⟼ (k \in X ⟼ 2^{nd} (i (j) (k))))$
12		inss1	$⊢ A \cap (K H (X) Y) \subseteq A$
13	12 6	sstrid	$⊢ φ \to A \cap (K H (X) Y) \subseteq ℝ^{X}$
14	2 13	ovncl	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \in [0, +∞]$
15	12	a1i	$⊢ φ \to A \cap (K H (X) Y) \subseteq A$
16	2 15 6	ovnssle	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \leq voln* (X) (A)$
17	5 14 16	ge0lere	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) \in ℝ$
18	6	ssdifssd	$⊢ φ \to A ∖ (K H (X) Y) \subseteq ℝ^{X}$
19	2 18	ovncl	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \in [0, +∞]$
20		difssd	$⊢ φ \to A ∖ (K H (X) Y) \subseteq A$
21	2 20 6	ovnssle	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A)$
22	5 19 21	ge0lere	$⊢ φ \to voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
23		rexadd	$⊢ (voln* (X) (A \cap (K H (X) Y)) \in ℝ \land voln* (X) (A ∖ (K H (X) Y)) \in ℝ) \to voln* (X) (A \cap (K H (X) Y)) +_{𝑒} voln* (X) (A ∖ (K H (X) Y)) = voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y))$
24	17 22 23	syl2anc	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) +_{𝑒} voln* (X) (A ∖ (K H (X) Y)) = voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y))$
25	2	adantr	$⊢ (φ \land e \in ℝ^{+}) \to X \in Fin$
26	3	ne0d	$⊢ φ \to X \neq \emptyset$
27	26	adantr	$⊢ (φ \land e \in ℝ^{+}) \to X \neq \emptyset$
28	6	adantr	$⊢ (φ \land e \in ℝ^{+}) \to A \subseteq ℝ^{X}$
29		simpr	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ^{+}$
30	25 27 28 29 7 8 9	ovncvrrp	$⊢ (φ \land e \in ℝ^{+}) \to \exists i i \in D (A) (e)$
31	25	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to X \in Fin$
32	3	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to K \in X$
33	4	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to Y \in ℝ$
34	29	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to e \in ℝ^{+}$
35	28	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to A \subseteq ℝ^{X}$
36		fveq1	$⊢ i = h \to i (j) = h (j)$
37	36	fveq2d	$⊢ i = h \to L (i (j)) = L (h (j))$
38	37	mpteq2dv	$⊢ i = h \to (j \in ℕ ⟼ L (i (j))) = (j \in ℕ ⟼ L (h (j)))$
39	38	fveq2d	$⊢ i = h \to sum^((j \in ℕ ⟼ L (i (j)))) = sum^((j \in ℕ ⟼ L (h (j))))$
40	39	breq1d	$⊢ i = h \to (sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r \leftrightarrow sum^((j \in ℕ ⟼ L (h (j)))) \leq voln* (X) (a) +_{𝑒} r)$
41	40	cbvrabv	$⊢ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\} = \{h \in C (a) \| sum^((j \in ℕ ⟼ L (h (j)))) \leq voln* (X) (a) +_{𝑒} r\}$
42	41	mpteq2i	$⊢ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\}) = (r \in ℝ^{+} ⟼ \{h \in C (a) \| sum^((j \in ℕ ⟼ L (h (j)))) \leq voln* (X) (a) +_{𝑒} r\})$
43	42	mpteq2i	$⊢ (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{i \in C (a) \| sum^((j \in ℕ ⟼ L (i (j)))) \leq voln* (X) (a) +_{𝑒} r\})) = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{h \in C (a) \| sum^((j \in ℕ ⟼ L (h (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
44	9 43	eqtri	$⊢ D = (a \in 𝒫 (ℝ^{X}) ⟼ (r \in ℝ^{+} ⟼ \{h \in C (a) \| sum^((j \in ℕ ⟼ L (h (j)))) \leq voln* (X) (a) +_{𝑒} r\}))$
45		simpr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to i \in D (A) (e)$
46	31 35 34 7 8 44 45 10 11	ovncvr2	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to (((B : ℕ ⟶ ℝ^{X} \land T : ℕ ⟶ ℝ^{X}) \land A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))) \land sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) +_{𝑒} e)$
47	46	simplld	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to (B : ℕ ⟶ ℝ^{X} \land T : ℕ ⟶ ℝ^{X})$
48	47	simpld	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to B : ℕ ⟶ ℝ^{X}$
49	47	simprd	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to T : ℕ ⟶ ℝ^{X}$
50	46	simplrd	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} [B (j) (k), T (j) (k))$
51	46	simprd	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) +_{𝑒} e$
52	5	adantr	$⊢ (φ \land e \in ℝ^{+}) \to voln* (X) (A) \in ℝ$
53	29	rpred	$⊢ (φ \land e \in ℝ^{+}) \to e \in ℝ$
54	52 53	rexaddd	$⊢ (φ \land e \in ℝ^{+}) \to voln* (X) (A) +_{𝑒} e = voln* (X) (A) + e$
55	54	adantr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to voln* (X) (A) +_{𝑒} e = voln* (X) (A) + e$
56	51 55	breqtrd	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to sum^((j \in ℕ ⟼ \prod_{k \in X} vol ([B (j) (k), T (j) (k))))) \leq voln* (X) (A) + e$
57	5	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to voln* (X) (A) \in ℝ$
58	17	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to voln* (X) (A \cap (K H (X) Y)) \in ℝ$
59	22	ad2antrr	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
60		eqid	$⊢ (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
61		eqid	$⊢ (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y))))) = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
62		eqid	$⊢ (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h))))) = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
63	1 31 32 33 34 48 49 50 56 57 58 59 60 61 62	hspmbllem2	$⊢ ((φ \land e \in ℝ^{+}) \land i \in D (A) (e)) \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e$
64	63	ex	$⊢ (φ \land e \in ℝ^{+}) \to (i \in D (A) (e) \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e)$
65	64	exlimdv	$⊢ (φ \land e \in ℝ^{+}) \to (\exists i i \in D (A) (e) \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e)$
66	30 65	mpd	$⊢ (φ \land e \in ℝ^{+}) \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e$
67	66	ralrimiva	$⊢ φ \to \forall e \in ℝ^{+} voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e$
68	17 22	readdcld	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \in ℝ$
69		alrple	$⊢ (voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \in ℝ \land voln* (X) (A) \in ℝ) \to (voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) \leftrightarrow \forall e \in ℝ^{+} voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e)$
70	68 5 69	syl2anc	$⊢ φ \to (voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) \leftrightarrow \forall e \in ℝ^{+} voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A) + e)$
71	67 70	mpbird	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) + voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A)$
72	24 71	eqbrtrd	$⊢ φ \to voln* (X) (A \cap (K H (X) Y)) +_{𝑒} voln* (X) (A ∖ (K H (X) Y)) \leq voln* (X) (A)$

Metamath Proof Explorer

Theorem hspmbllem3

Proof