Theorem hoidmvval0b

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

	Ref	Expression
Hypotheses	hoidmvval0b.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)$$
	hoidmvval0b.x	$$⊢\phi \to X\in \mathrm{Fin}$$
	hoidmvval0b.a	$$⊢\phi \to A:X⟶ℝ$$
Assertion	hoidmvval0b	$$⊢\phi \to AL\left(X\right)A=0$$

Proof

Step	Hyp	Ref	Expression
1		hoidmvval0b.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		hoidmvval0b.x	$$⊢\phi \to X\in \mathrm{Fin}$$
3		hoidmvval0b.a	$$⊢\phi \to A:X⟶ℝ$$
4		fveq2	$$⊢X=\varnothing \to L\left(X\right)=L\left(\varnothing \right)$$
5	4	oveqd	$$⊢X=\varnothing \to AL\left(X\right)A=AL\left(\varnothing \right)A$$
6	5	adantl	$$⊢\left(\phi \wedge X=\varnothing \right)\to AL\left(X\right)A=AL\left(\varnothing \right)A$$
7	3	adantr	$$⊢\left(\phi \wedge X=\varnothing \right)\to A:X⟶ℝ$$
8		feq2	$$⊢X=\varnothing \to \left(A:X⟶ℝ\leftrightarrow A:\varnothing ⟶ℝ\right)$$
9	8	adantl	$$⊢\left(\phi \wedge X=\varnothing \right)\to \left(A:X⟶ℝ\leftrightarrow A:\varnothing ⟶ℝ\right)$$
10	7 9	mpbid	$$⊢\left(\phi \wedge X=\varnothing \right)\to A:\varnothing ⟶ℝ$$
11	1 10 10	hoidmv0val	$$⊢\left(\phi \wedge X=\varnothing \right)\to AL\left(\varnothing \right)A=0$$
12	6 11	eqtrd	$$⊢\left(\phi \wedge X=\varnothing \right)\to AL\left(X\right)A=0$$
13		nfv	$$⊢Ⅎj\left(\phi \wedge \neg X=\varnothing \right)$$
14	2	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to X\in \mathrm{Fin}$$
15	3	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to A:X⟶ℝ$$
16		neqne	$$⊢\neg X=\varnothing \to X\ne \varnothing$$
17		n0	$$⊢X\ne \varnothing \leftrightarrow \exists jj\in X$$
18	16 17	sylib	$$⊢\neg X=\varnothing \to \exists jj\in X$$
19	18	adantl	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \exists jj\in X$$
20		simpr	$$⊢\left(\phi \wedge j\in X\right)\to j\in X$$
21	3	ffvelcdmda	$$⊢\left(\phi \wedge j\in X\right)\to A\left(j\right)\in ℝ$$
22		eqidd	$$⊢\left(\phi \wedge j\in X\right)\to A\left(j\right)=A\left(j\right)$$
23	21 22	eqled	$$⊢\left(\phi \wedge j\in X\right)\to A\left(j\right)\le A\left(j\right)$$
24	20 23	jca	$$⊢\left(\phi \wedge j\in X\right)\to \left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)$$
25	24	ex	$$⊢\phi \to \left(j\in X\to \left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)\right)$$
26	25	adantr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \left(j\in X\to \left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)\right)$$
27	26	eximdv	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \left(\exists jj\in X\to \exists j\left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)\right)$$
28	19 27	mpd	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \exists j\left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)$$
29		df-rex	$$⊢\exists j\in XA\left(j\right)\le A\left(j\right)\leftrightarrow \exists j\left(j\in X\wedge A\left(j\right)\le A\left(j\right)\right)$$
30	28 29	sylibr	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to \exists j\in XA\left(j\right)\le A\left(j\right)$$
31	13 1 14 15 15 30	hoidmvval0	$$⊢\left(\phi \wedge \neg X=\varnothing \right)\to AL\left(X\right)A=0$$
32	12 31	pm2.61dan	$$⊢\phi \to AL\left(X\right)A=0$$