Theorem vonn0ioo

Description: The n-dimensional Lebesgue measure of an open interval when the dimension of the space is nonzero. This is the first statement in Proposition 115G (d) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonn0ioo.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	vonn0ioo.n	$$⊢\phi \to X\ne \varnothing$$
	vonn0ioo.a	$$⊢\phi \to A:X⟶ℝ$$
	vonn0ioo.b	$$⊢\phi \to B:X⟶ℝ$$
	vonn0ioo.i	$$⊢I=\underset{k\in X}{⨉}\left(A\left(k\right),B\left(k\right)\right)$$
Assertion	vonn0ioo	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		vonn0ioo.x	$$⊢\phi \to X\in \mathrm{Fin}$$
2		vonn0ioo.n	$$⊢\phi \to X\ne \varnothing$$
3		vonn0ioo.a	$$⊢\phi \to A:X⟶ℝ$$
4		vonn0ioo.b	$$⊢\phi \to B:X⟶ℝ$$
5		vonn0ioo.i	$$⊢I=\underset{k\in X}{⨉}\left(A\left(k\right),B\left(k\right)\right)$$
6		fveq2	$$⊢j=k\to a\left(j\right)=a\left(k\right)$$
7		fveq2	$$⊢j=k\to b\left(j\right)=b\left(k\right)$$
8	6 7	oveq12d	$$⊢j=k\to \left[a\left(j\right),b\left(j\right)\right)=\left[a\left(k\right),b\left(k\right)\right)$$
9	8	fveq2d	$$⊢j=k\to vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)=vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)$$
10	9	cbvprodv	$$⊢\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)=\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)$$
11		ifeq2	$$⊢\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)=\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\to if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)=if\left(x=\varnothing ,0,\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\right)$$
12	10 11	ax-mp	$$⊢if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)=if\left(x=\varnothing ,0,\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\right)$$
13	12	a1i	$$⊢\left(a\in \left({ℝ}^x\right)\wedge b\in \left({ℝ}^x\right)\right)\to if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)=if\left(x=\varnothing ,0,\prod _{k\in x}vol\left(\left[a\left(k\right),b\left(k\right)\right)\right)\right)$$
14	13	mpoeq3ia	$$⊢\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)=\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)$$
15	14	mpteq2i	$$⊢\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)\right)=\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)$$
16	1 3 4 5 15	vonioo	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=A\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)\right)\left(X\right)B$$
17	15	fveq1i	$$⊢\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)\right)\left(X\right)=\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)\left(X\right)$$
18	17	oveqi	$$⊢A\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)\right)\left(X\right)B=A\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)\left(X\right)B$$
19	18	a1i	$$⊢\phi \to A\left(x\in \mathrm{Fin}⟼\left(a\in \left({ℝ}^x\right),b\in \left({ℝ}^x\right)⟼if\left(x=\varnothing ,0,\prod _{j\in x}vol\left(\left[a\left(j\right),b\left(j\right)\right)\right)\right)\right)\right)\left(X\right)B=A\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)\left(X\right)B$$
20	16 19	eqtrd	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=A\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)\left(X\right)B$$
21		eqid	$$⊢\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)=\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)$$
22	21 1 2 3 4	hoidmvn0val	$$⊢\phi \to A\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)\left(X\right)B=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$
23	20 22	eqtrd	$$⊢\phi \to \mathrm{voln}\left(X\right)\left(I\right)=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$