hoidmvcl

Description: The dimensional volume of a multidimensional half-open interval is a nonnegative real. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvcl.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvcl.x	$⊢ φ \to X \in Fin$
	hoidmvcl.a	$⊢ φ \to A : X ⟶ ℝ$
	hoidmvcl.b	$⊢ φ \to B : X ⟶ ℝ$
Assertion	hoidmvcl	$⊢ φ \to A L (X) B \in [0, +∞)$

Proof

Step	Hyp	Ref	Expression
1		hoidmvcl.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
2		hoidmvcl.x	$⊢ φ \to X \in Fin$
3		hoidmvcl.a	$⊢ φ \to A : X ⟶ ℝ$
4		hoidmvcl.b	$⊢ φ \to B : X ⟶ ℝ$
5	1 3 4 2	hoidmvval	$⊢ φ \to A L (X) B = if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k))))$
6		0e0icopnf	$⊢ 0 \in [0, +∞)$
7	6	a1i	$⊢ φ \to 0 \in [0, +∞)$
8		0xr	$⊢ 0 \in ℝ^{*}$
9	8	a1i	$⊢ φ \to 0 \in ℝ^{*}$
10		pnfxr	$⊢ +∞ \in ℝ^{*}$
11	10	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
12	3	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
13	4	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
14		volico	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
15	12 13 14	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) = if (A (k) < B (k), B (k) - A (k), 0)$
16	13 12	resubcld	$⊢ (φ \land k \in X) \to B (k) - A (k) \in ℝ$
17		0red	$⊢ (φ \land k \in X) \to 0 \in ℝ$
18	16 17	ifcld	$⊢ (φ \land k \in X) \to if (A (k) < B (k), B (k) - A (k), 0) \in ℝ$
19	15 18	eqeltrd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
20	2 19	fprodrecl	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) \in ℝ$
21	20	rexrd	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) \in ℝ^{*}$
22		nfv	$⊢ Ⅎ k φ$
23	13	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
24		icombl	$⊢ (A (k) \in ℝ \land B (k) \in ℝ^{*}) \to [A (k), B (k)) \in dom vol$
25	12 23 24	syl2anc	$⊢ (φ \land k \in X) \to [A (k), B (k)) \in dom vol$
26		volge0	$⊢ [A (k), B (k)) \in dom vol \to 0 \leq vol ([A (k), B (k)))$
27	25 26	syl	$⊢ (φ \land k \in X) \to 0 \leq vol ([A (k), B (k)))$
28	22 2 19 27	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in X} vol ([A (k), B (k)))$
29	20	ltpnfd	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) < +∞$
30	9 11 21 28 29	elicod	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) \in [0, +∞)$
31	7 30	ifcld	$⊢ φ \to if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k)))) \in [0, +∞)$
32	5 31	eqeltrd	$⊢ φ \to A L (X) B \in [0, +∞)$

Metamath Proof Explorer

Theorem hoidmvcl

Proof