Theorem hoidmvn0val

Description: The dimensional volume of a non-0-dimensional half-open interval. Definition 115A (c) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvn0val.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)$$
	hoidmvn0val.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	hoidmvn0val.n	$$⊢\phi \to X\ne \varnothing$$
	hoidmvn0val.a	$$⊢\phi \to A:X⟶ℝ$$
	hoidmvn0val.b	$$⊢\phi \to B:X⟶ℝ$$
Assertion	hoidmvn0val	$$⊢\phi \to AL\left(X\right)B=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hoidmvn0val.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)$$
2		hoidmvn0val.x	$$⊢\phi \to X\in \mathrm{Fin}$$
3		hoidmvn0val.n	$$⊢\phi \to X\ne \varnothing$$
4		hoidmvn0val.a	$$⊢\phi \to A:X⟶ℝ$$
5		hoidmvn0val.b	$$⊢\phi \to B:X⟶ℝ$$
6	1 4 5 2	hoidmvval	$$⊢\phi \to AL\left(X\right)B=if\left(X=\varnothing ,0,\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)$$
7	3	neneqd	$$⊢\phi \to \neg X=\varnothing$$
8	7	iffalsed	$$⊢\phi \to if\left(X=\varnothing ,0,\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$
9	6 8	eqtrd	$$⊢\phi \to AL\left(X\right)B=\prod _{k\in X}vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)$$