ovn0

Description: For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (ii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypothesis	ovn0.1	$⊢ φ \to X \in Fin$
	Assertion	ovn0	$⊢ φ \to voln* (X) (\emptyset) = 0$

Proof

Step	Hyp	Ref	Expression
1		ovn0.1	$⊢ φ \to X \in Fin$
2		0ss	$⊢ \emptyset \subseteq ℝ^{X}$
3	2	a1i	$⊢ φ \to \emptyset \subseteq ℝ^{X}$
4		0ss	$⊢ \emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
5	4	a1i	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \to \emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
6		id	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \to z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
7	5 6	jca	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \to (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
8		simpr	$⊢ (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))) \to z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
9	7 8	impbii	$⊢ z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
10	9	rexbii	$⊢ \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
11	10	rgenw	$⊢ \forall z \in ℝ^{*} (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))))$
12		rabbi	$⊢ \forall z \in ℝ^{} (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))) \leftrightarrow \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))) \leftrightarrow \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
13	11 12	mpbi	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (\emptyset \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \land z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))\}$
14	1 3 13	ovnval2	$⊢ φ \to voln* (X) (\emptyset) = if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <))$
15		simpr	$⊢ (φ \land X = \emptyset) \to X = \emptyset$
16	15	iftrued	$⊢ (φ \land X = \emptyset) \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)) = 0$
17		iffalse	$⊢ \neg X = \emptyset \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)) = inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)$
18	17	adantl	$⊢ (φ \land \neg X = \emptyset) \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)) = inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)$
19	1	adantr	$⊢ (φ \land \neg X = \emptyset) \to X \in Fin$
20		neqne	$⊢ \neg X = \emptyset \to X \neq \emptyset$
21	20	adantl	$⊢ (φ \land \neg X = \emptyset) \to X \neq \emptyset$
22		eqid	$⊢ \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\}$
23	14 17	sylan9eq	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (\emptyset) = inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)$
24	23	eqcomd	$⊢ (φ \land \neg X = \emptyset) \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <) = voln* (X) (\emptyset)$
25	1	ovnf	$⊢ φ \to voln* (X) : 𝒫 (ℝ^{X}) ⟶ [0, +∞]$
26		0elpw	$⊢ \emptyset \in 𝒫 (ℝ^{X})$
27	26	a1i	$⊢ φ \to \emptyset \in 𝒫 (ℝ^{X})$
28	25 27	ffvelcdmd	$⊢ φ \to voln* (X) (\emptyset) \in [0, +∞]$
29	28	adantr	$⊢ (φ \land \neg X = \emptyset) \to voln* (X) (\emptyset) \in [0, +∞]$
30	24 29	eqeltrd	$⊢ (φ \land \neg X = \emptyset) \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <) \in [0, +∞]$
31		eqidd	$⊢ m = l \to ⟨1, 0⟩ = ⟨1, 0⟩$
32	31	cbvmptv	$⊢ (m \in X ⟼ ⟨1, 0⟩) = (l \in X ⟼ ⟨1, 0⟩)$
33	32	a1i	$⊢ h = j \to (m \in X ⟼ ⟨1, 0⟩) = (l \in X ⟼ ⟨1, 0⟩)$
34	33	cbvmptv	$⊢ (h \in ℕ ⟼ (m \in X ⟼ ⟨1, 0⟩)) = (j \in ℕ ⟼ (l \in X ⟼ ⟨1, 0⟩))$
35	19 21 22 30 34	ovn0lem	$⊢ (φ \land \neg X = \emptyset) \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <) = 0$
36	18 35	eqtrd	$⊢ (φ \land \neg X = \emptyset) \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)) = 0$
37	16 36	pm2.61dan	$⊢ φ \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))\} ℝ^{} <)) = 0$
38	14 37	eqtrd	$⊢ φ \to voln* (X) (\emptyset) = 0$

Metamath Proof Explorer

Theorem ovn0

Proof