ovnval

Description: Value of the Lebesgue outer measure for a given finite dimension. (Contributed by Glauco Siliprandi, 11-Oct-2020)

		Ref	Expression
	Hypothesis	ovnval.1	$⊢ φ \to X \in Fin$
	Assertion	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)))))\} ℝ^{} <)))$

Proof

Step	Hyp	Ref	Expression
1		ovnval.1	$⊢ φ \to X \in Fin$
2		df-ovoln	$⊢ voln* = (x \in Fin ⟼ (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)))))\} ℝ^{} <))))$
3		oveq2	$⊢ x = X \to ℝ^{x} = ℝ^{X}$
4	3	pweqd	$⊢ x = X \to 𝒫 (ℝ^{x}) = 𝒫 (ℝ^{X})$
5		eqeq1	$⊢ x = X \to (x = \emptyset \leftrightarrow X = \emptyset)$
6		oveq2	$⊢ x = X \to {ℝ^{2}}^{x} = {ℝ^{2}}^{X}$
7	6	oveq1d	$⊢ x = X \to {({ℝ^{2}}^{x})}^{ℕ} = {({ℝ^{2}}^{X})}^{ℕ}$
8		ixpeq1	$⊢ x = X \to \underset{k \in x}{⨉} ([.) \circ i (j)) (k) = \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
9	8	iuneq2d	$⊢ x = X \to ⋃_{j \in ℕ} \underset{k \in x}{⨉} ([.) \circ i (j)) (k) = ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k)$
10	9	sseq2d	$⊢ x = X \to (y \subseteq ⋃_{j \in ℕ} \underset{k \in x}{⨉} ([.) \circ i (j)) (k) \leftrightarrow y \subseteq ⋃_{j \in ℕ} \underset{k \in X}{⨉} ([.) \circ i (j)) (k))$
11		simpl	$⊢ (x = X \land j \in ℕ) \to x = X$
12	11	prodeq1d	$⊢ (x = X \land j \in ℕ) \to \prod_{k \in x} vol (([.) \circ i (j)) (k)) = \prod_{k \in X} vol (([.) \circ i (j)) (k))$
13	12	mpteq2dva	$⊢ x = X \to (j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k))) = (j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))$
14	13	fveq2d	$⊢ x = X \to sum^((j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k)))) = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k))))$
15	14	eqeq2d	$⊢ x = X \to (z = sum^((j \in ℕ ⟼ \prod_{k \in x} vol (([.) \circ i (j)) (k)))) \leftrightarrow z = sum^((j \in ℕ ⟼ \prod_{k \in X} vol (([.) \circ i (j)) (k)))))$
16	10 15	anbi12d	$⊢ x = X \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 (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))))))$
17	7 16	rexeqbidv	$⊢ x = X \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})}^{ℕ}) (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))))))$
18	17	rabbidv	$⊢ x = X \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})}^{ℕ}) (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)))))\}$
19	18	infeq1d	$⊢ x = X \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 (\{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)))))\} ℝ^{} <)$
20	5 19	ifbieq2d	$⊢ x = X \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 (\{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)))))\} ℝ^{} <))$
21	4 20	mpteq12dv	$⊢ x = X \to (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)))))\} ℝ^{} <))) = (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)))))\} ℝ^{} <)))$
22		ovex	$⊢ ℝ^{X} \in V$
23	22	pwex	$⊢ 𝒫 (ℝ^{X}) \in V$
24	23	mptex	$⊢ (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)))))\} ℝ^{} <))) \in V$
25	24	a1i	$⊢ φ \to (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)))))\} ℝ^{} <))) \in V$
26	2 21 1 25	fvmptd3	$⊢ φ \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)))))\} ℝ^{} <)))$

Metamath Proof Explorer

Theorem ovnval

Proof