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	$$⊢\phi \to X\in \mathrm{Fin}$$
	vonhoi.a	$$⊢\phi \to A:X⟶ℝ$$
	vonhoi.b	$$⊢\phi \to B:X⟶ℝ$$
	vonhoi.c	$$⊢I=\underset{k\in X}{⨉}\left[A\left(k\right),B\left(k\right)\right)$$
	vonhoi.l	$$⊢L=\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\right)\right)\right)$$
Assertion	vonhoi	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=AL\left(X\right)B$$

Proof

Step	Hyp	Ref	Expression
1		vonhoi.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		vonhoi.a	$$⊢\phi \to A:X⟶ℝ$$
3		vonhoi.b	$$⊢\phi \to B:X⟶ℝ$$
4		vonhoi.c	$$⊢I=\underset{k\in X}{⨉}\left[A\left(k\right),B\left(k\right)\right)$$
5		vonhoi.l	$$⊢L=\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\right)\right)\right)$$
6		eqid	$$⊢\mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{dom}\mathrm{voln}\left(X\right)$$
7	1 6 2 3	hoimbl	$$⊢\phi \to \underset{k\in X}{⨉}\left[A\left(k\right),B\left(k\right)\right)\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
8	4 7	eqeltrid	$$⊢\phi \to I\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
9	1 8	mblvon	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=\mathrm{voln*}\left(X\right)\left(I\right)$$
10	1 2 3 4 5	ovnhoi	$$⊢\phi \to \mathrm{voln*}\left(X\right)\left(I\right)=AL\left(X\right)B$$
11	9 10	eqtrd	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=AL\left(X\right)B$$