hoidmvval

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

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

Proof

Step	Hyp	Ref	Expression
1		hoidmvval.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		hoidmvval.a	$⊢ φ \to A : X ⟶ ℝ$
3		hoidmvval.b	$⊢ φ \to B : X ⟶ ℝ$
4		hoidmvval.x	$⊢ φ \to X \in Fin$
5		oveq2	$⊢ x = X \to ℝ^{x} = ℝ^{X}$
6		eqeq1	$⊢ x = X \to (x = \emptyset \leftrightarrow X = \emptyset)$
7		prodeq1	$⊢ x = X \to \prod_{k \in x} vol ([a (k), b (k))) = \prod_{k \in X} vol ([a (k), b (k)))$
8	6 7	ifbieq2d	$⊢ x = X \to if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k)))) = if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k))))$
9	5 5 8	mpoeq123dv	$⊢ x = X \to (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))) = (a \in (ℝ^{X}), b \in (ℝ^{X}) ⟼ if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k)))))$
10		ovex	$⊢ ℝ^{X} \in V$
11	10 10	mpoex	$⊢ (a \in (ℝ^{X}), b \in (ℝ^{X}) ⟼ if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k))))) \in V$
12	11	a1i	$⊢ φ \to (a \in (ℝ^{X}), b \in (ℝ^{X}) ⟼ if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k))))) \in V$
13	1 9 4 12	fvmptd3	$⊢ φ \to L (X) = (a \in (ℝ^{X}), b \in (ℝ^{X}) ⟼ if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k)))))$
14		fveq1	$⊢ a = A \to a (k) = A (k)$
15	14	adantr	$⊢ (a = A \land b = B) \to a (k) = A (k)$
16		fveq1	$⊢ b = B \to b (k) = B (k)$
17	16	adantl	$⊢ (a = A \land b = B) \to b (k) = B (k)$
18	15 17	oveq12d	$⊢ (a = A \land b = B) \to [a (k), b (k)) = [A (k), B (k))$
19	18	fveq2d	$⊢ (a = A \land b = B) \to vol ([a (k), b (k))) = vol ([A (k), B (k)))$
20	19	prodeq2ad	$⊢ (a = A \land b = B) \to \prod_{k \in X} vol ([a (k), b (k))) = \prod_{k \in X} vol ([A (k), B (k)))$
21	20	ifeq2d	$⊢ (a = A \land b = B) \to if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k)))) = if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k))))$
22	21	adantl	$⊢ (φ \land (a = A \land b = B)) \to if (X = \emptyset, 0, \prod_{k \in X} vol ([a (k), b (k)))) = if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k))))$
23		reex	$⊢ ℝ \in V$
24	23	a1i	$⊢ φ \to ℝ \in V$
25		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to (A \in (ℝ^{X}) \leftrightarrow A : X ⟶ ℝ)$
26	24 4 25	syl2anc	$⊢ φ \to (A \in (ℝ^{X}) \leftrightarrow A : X ⟶ ℝ)$
27	2 26	mpbird	$⊢ φ \to A \in (ℝ^{X})$
28		elmapg	$⊢ (ℝ \in V \land X \in Fin) \to (B \in (ℝ^{X}) \leftrightarrow B : X ⟶ ℝ)$
29	24 4 28	syl2anc	$⊢ φ \to (B \in (ℝ^{X}) \leftrightarrow B : X ⟶ ℝ)$
30	3 29	mpbird	$⊢ φ \to B \in (ℝ^{X})$
31		c0ex	$⊢ 0 \in V$
32		prodex	$⊢ \prod_{k \in X} vol ([A (k), B (k))) \in V$
33	31 32	ifex	$⊢ if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k)))) \in V$
34	33	a1i	$⊢ φ \to if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k)))) \in V$
35	13 22 27 30 34	ovmpod	$⊢ φ \to A L (X) B = if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k))))$

Metamath Proof Explorer

Theorem hoidmvval

Proof