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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonn0hoi.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
	vonn0hoi.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	vonn0hoi.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
	vonn0hoi.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
Assertion	vonn0hoi	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vonn0hoi.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonn0hoi.n	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
3		vonn0hoi.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
4		vonn0hoi.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
5		vonn0hoi.i	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
6		eqid	⊢ ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
7	1 3 4 5 6	vonhoi	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) )
8	6 1 2 3 4	hoidmvn0val	⊢ ( 𝜑 → ( 𝐴 ( ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) ) ‘ 𝑋 ) 𝐵 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )
9	7 8	eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ∏ 𝑘 ∈ 𝑋 ( vol ‘ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ) )