hoidmvval0

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	hoidmvval0.p	$⊢ Ⅎ j φ$
	hoidmvval0.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidmvval0.x	$⊢ φ \to X \in Fin$
	hoidmvval0.a	$⊢ φ \to A : X ⟶ ℝ$
	hoidmvval0.b	$⊢ φ \to B : X ⟶ ℝ$
	hoidmvval0.j	$⊢ φ \to \exists j \in X B (j) \leq A (j)$
Assertion	hoidmvval0	$⊢ φ \to A L (X) B = 0$

Proof

Step	Hyp	Ref	Expression
1		hoidmvval0.p	$⊢ Ⅎ j φ$
2		hoidmvval0.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
3		hoidmvval0.x	$⊢ φ \to X \in Fin$
4		hoidmvval0.a	$⊢ φ \to A : X ⟶ ℝ$
5		hoidmvval0.b	$⊢ φ \to B : X ⟶ ℝ$
6		hoidmvval0.j	$⊢ φ \to \exists j \in X B (j) \leq A (j)$
7		id	$⊢ φ \to φ$
8		fveq2	$⊢ k = j \to B (k) = B (j)$
9		fveq2	$⊢ k = j \to A (k) = A (j)$
10	8 9	breq12d	$⊢ k = j \to (B (k) \leq A (k) \leftrightarrow B (j) \leq A (j))$
11	10	cbvrexvw	$⊢ \exists k \in X B (k) \leq A (k) \leftrightarrow \exists j \in X B (j) \leq A (j)$
12		rexn0	$⊢ \exists k \in X B (k) \leq A (k) \to X \neq \emptyset$
13	11 12	sylbir	$⊢ \exists j \in X B (j) \leq A (j) \to X \neq \emptyset$
14	6 13	syl	$⊢ φ \to X \neq \emptyset$
15	3	adantr	$⊢ (φ \land X \neq \emptyset) \to X \in Fin$
16		simpr	$⊢ (φ \land X \neq \emptyset) \to X \neq \emptyset$
17	4	adantr	$⊢ (φ \land X \neq \emptyset) \to A : X ⟶ ℝ$
18	5	adantr	$⊢ (φ \land X \neq \emptyset) \to B : X ⟶ ℝ$
19	2 15 16 17 18	hoidmvn0val	$⊢ (φ \land X \neq \emptyset) \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
20	6	adantr	$⊢ (φ \land X \neq \emptyset) \to \exists j \in X B (j) \leq A (j)$
21		nfv	$⊢ Ⅎ j X \neq \emptyset$
22	1 21	nfan	$⊢ Ⅎ j (φ \land X \neq \emptyset)$
23		nfv	$⊢ Ⅎ j \prod_{k \in X} vol ([A (k), B (k))) = 0$
24		nfv	$⊢ Ⅎ k (φ \land j \in X \land B (j) \leq A (j))$
25		nfcv	$⊢ \underline{Ⅎ} k vol ([A (j), B (j)))$
26	3	3ad2ant1	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to X \in Fin$
27	4	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
28	5	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
29		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
30	27 28 29	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
31	30	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
32	31	3ad2antl1	$⊢ ((φ \land j \in X \land B (j) \leq A (j)) \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
33	9 8	oveq12d	$⊢ k = j \to [A (k), B (k)) = [A (j), B (j))$
34	33	fveq2d	$⊢ k = j \to vol ([A (k), B (k))) = vol ([A (j), B (j)))$
35		simp2	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to j \in X$
36	4	ffvelcdmda	$⊢ (φ \land j \in X) \to A (j) \in ℝ$
37	36	3adant3	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to A (j) \in ℝ$
38	5	ffvelcdmda	$⊢ (φ \land j \in X) \to B (j) \in ℝ$
39	38	3adant3	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to B (j) \in ℝ$
40		volico	$⊢ (A (j) \in ℝ \land B (j) \in ℝ) \to vol ([A (j), B (j))) = if (A (j) < B (j), B (j) - A (j), 0)$
41	37 39 40	syl2anc	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to vol ([A (j), B (j))) = if (A (j) < B (j), B (j) - A (j), 0)$
42		simp3	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to B (j) \leq A (j)$
43	39 37	lenltd	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to (B (j) \leq A (j) \leftrightarrow \neg A (j) < B (j))$
44	42 43	mpbid	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to \neg A (j) < B (j)$
45	44	iffalsed	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to if (A (j) < B (j), B (j) - A (j), 0) = 0$
46	41 45	eqtrd	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to vol ([A (j), B (j))) = 0$
47	24 25 26 32 34 35 46	fprod0	$⊢ (φ \land j \in X \land B (j) \leq A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
48	47	3adant1r	$⊢ ((φ \land X \neq \emptyset) \land j \in X \land B (j) \leq A (j)) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
49	48	3exp	$⊢ (φ \land X \neq \emptyset) \to (j \in X \to (B (j) \leq A (j) \to \prod_{k \in X} vol ([A (k), B (k))) = 0))$
50	22 23 49	rexlimd	$⊢ (φ \land X \neq \emptyset) \to (\exists j \in X B (j) \leq A (j) \to \prod_{k \in X} vol ([A (k), B (k))) = 0)$
51	20 50	mpd	$⊢ (φ \land X \neq \emptyset) \to \prod_{k \in X} vol ([A (k), B (k))) = 0$
52		eqidd	$⊢ (φ \land X \neq \emptyset) \to 0 = 0$
53	19 51 52	3eqtrd	$⊢ (φ \land X \neq \emptyset) \to A L (X) B = 0$
54	7 14 53	syl2anc	$⊢ φ \to A L (X) B = 0$

Metamath Proof Explorer

Theorem hoidmvval0

Proof