Theorem hoidmv0val

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

	Ref	Expression
Hypotheses	hoidmv0val.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)$$
	hoidmv0val.a	$$⊢\phi \to A:\varnothing ⟶ℝ$$
	hoidmv0val.b	$$⊢\phi \to B:\varnothing ⟶ℝ$$
Assertion	hoidmv0val	$$⊢\phi \to AL\left(\varnothing \right)B=0$$

Proof

Step	Hyp	Ref	Expression
1		hoidmv0val.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		hoidmv0val.a	$$⊢\phi \to A:\varnothing ⟶ℝ$$
3		hoidmv0val.b	$$⊢\phi \to B:\varnothing ⟶ℝ$$
4		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
5	4	a1i	$$⊢\phi \to \varnothing \in \mathrm{Fin}$$
6	1 2 3 5	hoidmvval	$$⊢\phi \to AL\left(\varnothing \right)B=if\left(\varnothing =\varnothing ,0,\prod _{k\in \varnothing }vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)$$
7		eqid	$$⊢\varnothing =\varnothing$$
8		iftrue	$$⊢\varnothing =\varnothing \to if\left(\varnothing =\varnothing ,0,\prod _{k\in \varnothing }vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)=0$$
9	7 8	ax-mp	$$⊢if\left(\varnothing =\varnothing ,0,\prod _{k\in \varnothing }vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)=0$$
10	9	a1i	$$⊢\phi \to if\left(\varnothing =\varnothing ,0,\prod _{k\in \varnothing }vol\left(\left[A\left(k\right),B\left(k\right)\right)\right)\right)=0$$
11	6 10	eqtrd	$$⊢\phi \to AL\left(\varnothing \right)B=0$$