ovnval2

Description: Value of the Lebesgue outer measure of a subset A of the space of multidimensional real numbers. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	ovnval2.1	$⊢ φ \to X \in Fin$
	ovnval2.2	$⊢ φ \to A \subseteq ℝ^{X}$
	ovnval2.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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)))))\}$
Assertion	ovnval2	$⊢ φ \to voln* (X) (A) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$

Proof

Step	Hyp	Ref	Expression
1		ovnval2.1	$⊢ φ \to X \in Fin$
2		ovnval2.2	$⊢ φ \to A \subseteq ℝ^{X}$
3		ovnval2.3	$⊢ M = \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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)))))\}$
4	1	ovnval	$⊢ φ \to voln* (X) = (y \in 𝒫 (ℝ^{X}) ⟼ if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)))$
5		biidd	$⊢ y = A \to (X = \emptyset \leftrightarrow X = \emptyset)$
6		sseq1	$⊢ y = A \to (y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k) \leftrightarrow A \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
7	6	anbi1d	$⊢ y = A \to ((y \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 (A \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	7	rexbidv	$⊢ y = A \to (\exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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 \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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))))))$
9	8	rabbidv	$⊢ y = A \to \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} = \{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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 3	eqtr4di	$⊢ y = A \to \{z \in ℝ^{*} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} = M$
11	10	infeq1d	$⊢ y = A \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <) = inf (M ℝ^{*} <)$
12	5 11	ifbieq2d	$⊢ y = A \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$
13	12	adantl	$⊢ (φ \land y = A) \to if (X = \emptyset, 0, inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (y \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)))))\} ℝ^{} <)) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$
14		ovexd	$⊢ φ \to ℝ^{X} \in V$
15	14 2	ssexd	$⊢ φ \to A \in V$
16		elpwg	$⊢ A \in V \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
17	15 16	syl	$⊢ φ \to (A \in 𝒫 (ℝ^{X}) \leftrightarrow A \subseteq ℝ^{X})$
18	2 17	mpbird	$⊢ φ \to A \in 𝒫 (ℝ^{X})$
19		c0ex	$⊢ 0 \in V$
20	19	a1i	$⊢ φ \to 0 \in V$
21	3	infeq1i	$⊢ inf (M ℝ^{} <) = inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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)))))\} ℝ^{*} <)$
22		xrltso	$⊢ < Or ℝ^{*}$
23	22	infex	$⊢ inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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)))))\} ℝ^{} <) \in V$
24	23	a1i	$⊢ φ \to inf (\{z \in ℝ^{} \| \exists i \in ({({ℝ^{2}}^{X})}^{ℕ}) (A \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)))))\} ℝ^{} <) \in V$
25	21 24	eqeltrid	$⊢ φ \to inf (M ℝ^{*} <) \in V$
26	20 25	ifcld	$⊢ φ \to if (X = \emptyset, 0, inf (M ℝ^{*} <)) \in V$
27	4 13 18 26	fvmptd	$⊢ φ \to voln* (X) (A) = if (X = \emptyset, 0, inf (M ℝ^{*} <))$

Metamath Proof Explorer

Theorem ovnval2

Proof