hsphoidmvle

Description: The dimensional volume of a half-open interval intersected with a half-space, is less than or equal to the dimensional volume of the original half-open interval. Used in the last inequality of step (e) of Lemma 115B of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hsphoidmvle.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hsphoidmvle.x	$⊢ φ \to X \in Fin$
	hsphoidmvle.z	$⊢ φ \to Z \in (X ∖ Y)$
	hsphoidmvle.y	$⊢ X = Y \cup \{Z\}$
	hsphoidmvle.c	$⊢ φ \to C \in ℝ$
	hsphoidmvle.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (j \in X ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
	hsphoidmvle.a	$⊢ φ \to A : X ⟶ ℝ$
	hsphoidmvle.b	$⊢ φ \to B : X ⟶ ℝ$
Assertion	hsphoidmvle	$⊢ φ \to A L (X) H (C) (B) \leq A L (X) B$

Proof

Step	Hyp	Ref	Expression
1		hsphoidmvle.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		hsphoidmvle.x	$⊢ φ \to X \in Fin$
3		hsphoidmvle.z	$⊢ φ \to Z \in (X ∖ Y)$
4		hsphoidmvle.y	$⊢ X = Y \cup \{Z\}$
5		hsphoidmvle.c	$⊢ φ \to C \in ℝ$
6		hsphoidmvle.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (j \in X ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
7		hsphoidmvle.a	$⊢ φ \to A : X ⟶ ℝ$
8		hsphoidmvle.b	$⊢ φ \to B : X ⟶ ℝ$
9	3	eldifad	$⊢ φ \to Z \in X$
10	7 9	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
11	8 9	ffvelcdmd	$⊢ φ \to B (Z) \in ℝ$
12	11 5	ifcld	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \in ℝ$
13		volicore	$⊢ (A (Z) \in ℝ \land if (B (Z) \leq C, B (Z), C) \in ℝ) \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \in ℝ$
14	10 12 13	syl2anc	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \in ℝ$
15		volicore	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ) \to vol ([A (Z), B (Z))) \in ℝ$
16	10 11 15	syl2anc	$⊢ φ \to vol ([A (Z), B (Z))) \in ℝ$
17		difssd	$⊢ φ \to X ∖ \{Z\} \subseteq X$
18		ssfi	$⊢ (X \in Fin \land X ∖ \{Z\} \subseteq X) \to X ∖ \{Z\} \in Fin$
19	2 17 18	syl2anc	$⊢ φ \to X ∖ \{Z\} \in Fin$
20		eldifi	$⊢ k \in (X ∖ \{Z\}) \to k \in X$
21	20	adantl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to k \in X$
22	7	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
23	8	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
24		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
25	22 23 24	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
26	21 25	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to vol ([A (k), B (k))) \in ℝ$
27	19 26	fprodrecl	$⊢ φ \to \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))) \in ℝ$
28		nfv	$⊢ Ⅎ k φ$
29	21 22	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to A (k) \in ℝ$
30	21 23	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B (k) \in ℝ$
31	30	rexrd	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B (k) \in ℝ^{*}$
32		icombl	$⊢ (A (k) \in ℝ \land B (k) \in ℝ^{*}) \to [A (k), B (k)) \in dom vol$
33	29 31 32	syl2anc	$⊢ (φ \land k \in (X ∖ \{Z\})) \to [A (k), B (k)) \in dom vol$
34		volge0	$⊢ [A (k), B (k)) \in dom vol \to 0 \leq vol ([A (k), B (k)))$
35	33 34	syl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to 0 \leq vol ([A (k), B (k)))$
36	28 19 26 35	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
37	12	rexrd	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \in ℝ^{*}$
38		icombl	$⊢ (A (Z) \in ℝ \land if (B (Z) \leq C, B (Z), C) \in ℝ^{*}) \to [A (Z), if (B (Z) \leq C, B (Z), C)) \in dom vol$
39	10 37 38	syl2anc	$⊢ φ \to [A (Z), if (B (Z) \leq C, B (Z), C)) \in dom vol$
40	11	rexrd	$⊢ φ \to B (Z) \in ℝ^{*}$
41		icombl	$⊢ (A (Z) \in ℝ \land B (Z) \in ℝ^{*}) \to [A (Z), B (Z)) \in dom vol$
42	10 40 41	syl2anc	$⊢ φ \to [A (Z), B (Z)) \in dom vol$
43	10	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
44	10	leidd	$⊢ φ \to A (Z) \leq A (Z)$
45		min1	$⊢ (B (Z) \in ℝ \land C \in ℝ) \to if (B (Z) \leq C, B (Z), C) \leq B (Z)$
46	11 5 45	syl2anc	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \leq B (Z)$
47		icossico	$⊢ ((A (Z) \in ℝ^{} \land B (Z) \in ℝ^{}) \land (A (Z) \leq A (Z) \land if (B (Z) \leq C, B (Z), C) \leq B (Z))) \to [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), B (Z))$
48	43 40 44 46 47	syl22anc	$⊢ φ \to [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), B (Z))$
49		volss	$⊢ ([A (Z), if (B (Z) \leq C, B (Z), C)) \in dom vol \land [A (Z), B (Z)) \in dom vol \land [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), B (Z))) \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \leq vol ([A (Z), B (Z)))$
50	39 42 48 49	syl3anc	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \leq vol ([A (Z), B (Z)))$
51	14 16 27 36 50	lemul1ad	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))) \leq vol ([A (Z), B (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
52	9	ne0d	$⊢ φ \to X \neq \emptyset$
53	6 5 2 8	hsphoif	$⊢ φ \to H (C) (B) : X ⟶ ℝ$
54	1 2 52 7 53	hoidmvn0val	$⊢ φ \to A L (X) H (C) (B) = \prod_{k \in X} vol ([A (k), H (C) (B) (k)))$
55	53	ffvelcdmda	$⊢ (φ \land k \in X) \to H (C) (B) (k) \in ℝ$
56		volicore	$⊢ (A (k) \in ℝ \land H (C) (B) (k) \in ℝ) \to vol ([A (k), H (C) (B) (k))) \in ℝ$
57	22 55 56	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), H (C) (B) (k))) \in ℝ$
58	57	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), H (C) (B) (k))) \in ℂ$
59		fveq2	$⊢ k = Z \to A (k) = A (Z)$
60		fveq2	$⊢ k = Z \to H (C) (B) (k) = H (C) (B) (Z)$
61	59 60	oveq12d	$⊢ k = Z \to [A (k), H (C) (B) (k)) = [A (Z), H (C) (B) (Z))$
62	61	fveq2d	$⊢ k = Z \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), H (C) (B) (Z)))$
63	62	adantl	$⊢ (φ \land k = Z) \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), H (C) (B) (Z)))$
64	6 5 2 8 9	hsphoival	$⊢ φ \to H (C) (B) (Z) = if (Z \in Y, B (Z), if (B (Z) \leq C, B (Z), C))$
65	3	eldifbd	$⊢ φ \to \neg Z \in Y$
66	65	iffalsed	$⊢ φ \to if (Z \in Y, B (Z), if (B (Z) \leq C, B (Z), C)) = if (B (Z) \leq C, B (Z), C)$
67	64 66	eqtrd	$⊢ φ \to H (C) (B) (Z) = if (B (Z) \leq C, B (Z), C)$
68	67	oveq2d	$⊢ φ \to [A (Z), H (C) (B) (Z)) = [A (Z), if (B (Z) \leq C, B (Z), C))$
69	68	fveq2d	$⊢ φ \to vol ([A (Z), H (C) (B) (Z))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
70	69	adantr	$⊢ (φ \land k = Z) \to vol ([A (Z), H (C) (B) (Z))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
71	63 70	eqtrd	$⊢ (φ \land k = Z) \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
72	2 58 9 71	fprodsplit1	$⊢ φ \to \prod_{k \in X} vol ([A (k), H (C) (B) (k))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (C) (B) (k)))$
73	5	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to C \in ℝ$
74	2	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to X \in Fin$
75	8	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B : X ⟶ ℝ$
76	6 73 74 75 21	hsphoival	$⊢ (φ \land k \in (X ∖ \{Z\})) \to H (C) (B) (k) = if (k \in Y, B (k), if (B (k) \leq C, B (k), C))$
77	20 4	eleqtrdi	$⊢ k \in (X ∖ \{Z\}) \to k \in (Y \cup \{Z\})$
78		eldifn	$⊢ k \in (X ∖ \{Z\}) \to \neg k \in \{Z\}$
79		elunnel2	$⊢ (k \in (Y \cup \{Z\}) \land \neg k \in \{Z\}) \to k \in Y$
80	77 78 79	syl2anc	$⊢ k \in (X ∖ \{Z\}) \to k \in Y$
81	80	adantl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to k \in Y$
82	81	iftrued	$⊢ (φ \land k \in (X ∖ \{Z\})) \to if (k \in Y, B (k), if (B (k) \leq C, B (k), C)) = B (k)$
83	76 82	eqtrd	$⊢ (φ \land k \in (X ∖ \{Z\})) \to H (C) (B) (k) = B (k)$
84	83	oveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to [A (k), H (C) (B) (k)) = [A (k), B (k))$
85	84	fveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to vol ([A (k), H (C) (B) (k))) = vol ([A (k), B (k)))$
86	85	prodeq2dv	$⊢ φ \to \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (C) (B) (k))) = \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
87	86	oveq2d	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (C) (B) (k))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
88	54 72 87	3eqtrd	$⊢ φ \to A L (X) H (C) (B) = vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
89	1 7 8 2	hoidmvval	$⊢ φ \to A L (X) B = if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k))))$
90	52	neneqd	$⊢ φ \to \neg X = \emptyset$
91	90	iffalsed	$⊢ φ \to if (X = \emptyset, 0, \prod_{k \in X} vol ([A (k), B (k)))) = \prod_{k \in X} vol ([A (k), B (k)))$
92	25	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℂ$
93		fveq2	$⊢ k = Z \to B (k) = B (Z)$
94	59 93	oveq12d	$⊢ k = Z \to [A (k), B (k)) = [A (Z), B (Z))$
95	94	fveq2d	$⊢ k = Z \to vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
96	95	adantl	$⊢ (φ \land k = Z) \to vol ([A (k), B (k))) = vol ([A (Z), B (Z)))$
97	2 92 9 96	fprodsplit1	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = vol ([A (Z), B (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
98	89 91 97	3eqtrd	$⊢ φ \to A L (X) B = vol ([A (Z), B (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
99	88 98	breq12d	$⊢ φ \to (A L (X) H (C) (B) \leq A L (X) B \leftrightarrow vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))) \leq vol ([A (Z), B (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))))$
100	51 99	mpbird	$⊢ φ \to A L (X) H (C) (B) \leq A L (X) B$

Metamath Proof Explorer

Theorem hsphoidmvle

Proof