hoidifhspdmvle

Description: The dimensional volume of the difference of a half-open interval and a half-space is less than or equal to the dimensional volume of the whole half-open interval. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hoidifhspdmvle.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hoidifhspdmvle.x	$⊢ φ \to X \in Fin$
	hoidifhspdmvle.a	$⊢ φ \to A : X ⟶ ℝ$
	hoidifhspdmvle.b	$⊢ φ \to B : X ⟶ ℝ$
	hoidifhspdmvle.k	$⊢ φ \to K \in X$
	hoidifhspdmvle.d	$⊢ D = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
	hoidifhspdmvle.y	$⊢ φ \to Y \in ℝ$
Assertion	hoidifhspdmvle	$⊢ φ \to D (Y) (A) L (X) B \leq A L (X) B$

Proof

Step	Hyp	Ref	Expression
1		hoidifhspdmvle.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		hoidifhspdmvle.x	$⊢ φ \to X \in Fin$
3		hoidifhspdmvle.a	$⊢ φ \to A : X ⟶ ℝ$
4		hoidifhspdmvle.b	$⊢ φ \to B : X ⟶ ℝ$
5		hoidifhspdmvle.k	$⊢ φ \to K \in X$
6		hoidifhspdmvle.d	$⊢ D = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
7		hoidifhspdmvle.y	$⊢ φ \to Y \in ℝ$
8		nfv	$⊢ Ⅎ k φ$
9	6 7 2 3	hoidifhspf	$⊢ φ \to D (Y) (A) : X ⟶ ℝ$
10	9	ffvelcdmda	$⊢ (φ \land k \in X) \to D (Y) (A) (k) \in ℝ$
11	4	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
12		volicore	$⊢ (D (Y) (A) (k) \in ℝ \land B (k) \in ℝ) \to vol ([D (Y) (A) (k), B (k))) \in ℝ$
13	10 11 12	syl2anc	$⊢ (φ \land k \in X) \to vol ([D (Y) (A) (k), B (k))) \in ℝ$
14	11	rexrd	$⊢ (φ \land k \in X) \to B (k) \in ℝ^{*}$
15		icombl	$⊢ (D (Y) (A) (k) \in ℝ \land B (k) \in ℝ^{*}) \to [D (Y) (A) (k), B (k)) \in dom vol$
16	10 14 15	syl2anc	$⊢ (φ \land k \in X) \to [D (Y) (A) (k), B (k)) \in dom vol$
17		volge0	$⊢ [D (Y) (A) (k), B (k)) \in dom vol \to 0 \leq vol ([D (Y) (A) (k), B (k)))$
18	16 17	syl	$⊢ (φ \land k \in X) \to 0 \leq vol ([D (Y) (A) (k), B (k)))$
19	3	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
20		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
21	19 11 20	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
22		icombl	$⊢ (A (k) \in ℝ \land B (k) \in ℝ^{*}) \to [A (k), B (k)) \in dom vol$
23	19 14 22	syl2anc	$⊢ (φ \land k \in X) \to [A (k), B (k)) \in dom vol$
24	19	rexrd	$⊢ (φ \land k \in X) \to A (k) \in ℝ^{*}$
25	7	adantr	$⊢ (φ \land k \in X) \to Y \in ℝ$
26	25	adantr	$⊢ ((φ \land k \in X) \land k = K) \to Y \in ℝ$
27	19	adantr	$⊢ ((φ \land k \in X) \land k = K) \to A (k) \in ℝ$
28		max2	$⊢ (Y \in ℝ \land A (k) \in ℝ) \to A (k) \leq if (Y \leq A (k), A (k), Y)$
29	26 27 28	syl2anc	$⊢ ((φ \land k \in X) \land k = K) \to A (k) \leq if (Y \leq A (k), A (k), Y)$
30	2	adantr	$⊢ (φ \land k \in X) \to X \in Fin$
31	3	adantr	$⊢ (φ \land k \in X) \to A : X ⟶ ℝ$
32		simpr	$⊢ (φ \land k \in X) \to k \in X$
33	6 25 30 31 32	hoidifhspval3	$⊢ (φ \land k \in X) \to D (Y) (A) (k) = if (k = K, if (Y \leq A (k), A (k), Y), A (k))$
34	33	adantr	$⊢ ((φ \land k \in X) \land k = K) \to D (Y) (A) (k) = if (k = K, if (Y \leq A (k), A (k), Y), A (k))$
35		iftrue	$⊢ k = K \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = if (Y \leq A (k), A (k), Y)$
36	35	adantl	$⊢ ((φ \land k \in X) \land k = K) \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = if (Y \leq A (k), A (k), Y)$
37	34 36	eqtr2d	$⊢ ((φ \land k \in X) \land k = K) \to if (Y \leq A (k), A (k), Y) = D (Y) (A) (k)$
38	29 37	breqtrd	$⊢ ((φ \land k \in X) \land k = K) \to A (k) \leq D (Y) (A) (k)$
39	19	leidd	$⊢ (φ \land k \in X) \to A (k) \leq A (k)$
40	39	adantr	$⊢ ((φ \land k \in X) \land \neg k = K) \to A (k) \leq A (k)$
41	33	adantr	$⊢ ((φ \land k \in X) \land \neg k = K) \to D (Y) (A) (k) = if (k = K, if (Y \leq A (k), A (k), Y), A (k))$
42		iffalse	$⊢ \neg k = K \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = A (k)$
43	42	adantl	$⊢ ((φ \land k \in X) \land \neg k = K) \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = A (k)$
44	41 43	eqtr2d	$⊢ ((φ \land k \in X) \land \neg k = K) \to A (k) = D (Y) (A) (k)$
45	40 44	breqtrd	$⊢ ((φ \land k \in X) \land \neg k = K) \to A (k) \leq D (Y) (A) (k)$
46	38 45	pm2.61dan	$⊢ (φ \land k \in X) \to A (k) \leq D (Y) (A) (k)$
47	11	leidd	$⊢ (φ \land k \in X) \to B (k) \leq B (k)$
48		icossico	$⊢ ((A (k) \in ℝ^{} \land B (k) \in ℝ^{}) \land (A (k) \leq D (Y) (A) (k) \land B (k) \leq B (k))) \to [D (Y) (A) (k), B (k)) \subseteq [A (k), B (k))$
49	24 14 46 47 48	syl22anc	$⊢ (φ \land k \in X) \to [D (Y) (A) (k), B (k)) \subseteq [A (k), B (k))$
50		volss	$⊢ ([D (Y) (A) (k), B (k)) \in dom vol \land [A (k), B (k)) \in dom vol \land [D (Y) (A) (k), B (k)) \subseteq [A (k), B (k))) \to vol ([D (Y) (A) (k), B (k))) \leq vol ([A (k), B (k)))$
51	16 23 49 50	syl3anc	$⊢ (φ \land k \in X) \to vol ([D (Y) (A) (k), B (k))) \leq vol ([A (k), B (k)))$
52	8 2 13 18 21 51	fprodle	$⊢ φ \to \prod_{k \in X} vol ([D (Y) (A) (k), B (k))) \leq \prod_{k \in X} vol ([A (k), B (k)))$
53	5	ne0d	$⊢ φ \to X \neq \emptyset$
54	1 2 53 9 4	hoidmvn0val	$⊢ φ \to D (Y) (A) L (X) B = \prod_{k \in X} vol ([D (Y) (A) (k), B (k)))$
55	1 2 53 3 4	hoidmvn0val	$⊢ φ \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
56	54 55	breq12d	$⊢ φ \to (D (Y) (A) L (X) B \leq A L (X) B \leftrightarrow \prod_{k \in X} vol ([D (Y) (A) (k), B (k))) \leq \prod_{k \in X} vol ([A (k), B (k))))$
57	52 56	mpbird	$⊢ φ \to D (Y) (A) L (X) B \leq A L (X) B$

Metamath Proof Explorer

Theorem hoidifhspdmvle

Proof