Theorem vonhoi

Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). A direct consequence of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonhoi.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonhoi.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
	vonhoi.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
	vonhoi.c	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
	vonhoi.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
Assertion	vonhoi	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		vonhoi.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonhoi.a	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
3		vonhoi.b	⊢ ( 𝜑 → 𝐵 : 𝑋 ⟶ ℝ )
4		vonhoi.c	⊢ 𝐼 = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
5		vonhoi.l	⊢ 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘 ∈ 𝑥 ( vol ‘ ( ( 𝑎 ‘ 𝑘 ) [,) ( 𝑏 ‘ 𝑘 ) ) ) ) ) )
6		eqid	⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
7	1 6 2 3	hoimbl	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) ∈ dom ( voln ‘ 𝑋 ) )
8	4 7	eqeltrid	⊢ ( 𝜑 → 𝐼 ∈ dom ( voln ‘ 𝑋 ) )
9	1 8	mblvon	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) )
10	1 2 3 4 5	ovnhoi	⊢ ( 𝜑 → ( ( voln* ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )
11	9 10	eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐼 ) = ( 𝐴 ( 𝐿 ‘ 𝑋 ) 𝐵 ) )