Metamath Proof Explorer

Theorem vonn0hoi

Description: The Lebesgue outer measure of a multidimensional half-open interval when the dimension of the space is nonzero. (Contributed by Glauco Siliprandi, 8-Apr-2021)

		Ref	Expression
	Hypotheses	vonn0hoi.x	$⊢ φ \to X \in Fin$
		vonn0hoi.n	$⊢ φ \to X \neq \emptyset$
		vonn0hoi.a	$⊢ φ \to A : X ⟶ ℝ$
		vonn0hoi.b	$⊢ φ \to B : X ⟶ ℝ$
		vonn0hoi.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
	Assertion	vonn0hoi	$⊢ φ \to voln (X) (I) = \prod_{k \in X} vol ([A (k), B (k)))$

Proof

Step	Hyp	Ref	Expression
1		vonn0hoi.x	$⊢ φ \to X \in Fin$
2		vonn0hoi.n	$⊢ φ \to X \neq \emptyset$
3		vonn0hoi.a	$⊢ φ \to A : X ⟶ ℝ$
4		vonn0hoi.b	$⊢ φ \to B : X ⟶ ℝ$
5		vonn0hoi.i	$⊢ I = \underset{k \in X}{⨉} [A (k), B (k))$
6		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))))))$
7	1 3 4 5 6	vonhoi	$⊢ φ \to voln (X) (I) = A (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) (X) B$
8	6 1 2 3 4	hoidmvn0val	$⊢ φ \to A (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))))) (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
9	7 8	eqtrd	$⊢ φ \to voln (X) (I) = \prod_{k \in X} vol ([A (k), B (k)))$