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 ⊢ φ → X ∈ Fin
vonn0hoi.n ⊢ φ → X ≠ ∅
vonn0hoi.a ⊢ φ → A : X ⟶ ℝ
vonn0hoi.b ⊢ φ → B : X ⟶ ℝ
vonn0hoi.i ⊢ I = ⨉ k ∈ X A ⁡ k B ⁡ k
Assertion vonn0hoi ⊢ φ → voln ⁡ X ⁡ I = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k

Proof

Step Hyp Ref Expression
1 vonn0hoi.x ⊢ φ → X ∈ Fin
2 vonn0hoi.n ⊢ φ → X ≠ ∅
3 vonn0hoi.a ⊢ φ → A : X ⟶ ℝ
4 vonn0hoi.b ⊢ φ → B : X ⟶ ℝ
5 vonn0hoi.i ⊢ I = ⨉ k ∈ X A ⁡ k B ⁡ k
6 eqid ⊢ x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k = x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k
7 1 3 4 5 6 vonhoi ⊢ φ → voln ⁡ X ⁡ I = A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B
8 6 1 2 3 4 hoidmvn0val ⊢ φ → A x ∈ Fin ⟼ a ∈ ℝ x , b ∈ ℝ x ⟼ if x = ∅ 0 ∏ k ∈ x vol ⁡ a ⁡ k b ⁡ k ⁡ X B = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k
9 7 8 eqtrd ⊢ φ → voln ⁡ X ⁡ I = ∏ k ∈ X vol ⁡ A ⁡ k B ⁡ k