hsphoidmvle2

Description: The dimensional volume of a half-open interval intersected with a two half-spaces. Used in the last inequality of step (c) of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		hsphoidmvle2.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		hsphoidmvle2.x	$⊢ φ \to X \in Fin$
3		hsphoidmvle2.z	$⊢ φ \to Z \in (X ∖ Y)$
4		hsphoidmvle2.y	$⊢ X = Y \cup \{Z\}$
5		hsphoidmvle2.c	$⊢ φ \to C \in ℝ$
6		hsphoidmvle2.d	$⊢ φ \to D \in ℝ$
7		hsphoidmvle2.e	$⊢ φ \to C \leq D$
8		hsphoidmvle2.h	$⊢ H = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (j \in X ⟼ if (j \in Y, c (j), if (c (j) \leq x, c (j), x)))))$
9		hsphoidmvle2.a	$⊢ φ \to A : X ⟶ ℝ$
10		hsphoidmvle2.b	$⊢ φ \to B : X ⟶ ℝ$
11	3	eldifad	$⊢ φ \to Z \in X$
12	9 11	ffvelcdmd	$⊢ φ \to A (Z) \in ℝ$
13	10 11	ffvelcdmd	$⊢ φ \to B (Z) \in ℝ$
14	13 5	ifcld	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \in ℝ$
15		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 ℝ$
16	12 14 15	syl2anc	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \in ℝ$
17	13 6	ifcld	$⊢ φ \to if (B (Z) \leq D, B (Z), D) \in ℝ$
18		volicore	$⊢ (A (Z) \in ℝ \land if (B (Z) \leq D, B (Z), D) \in ℝ) \to vol ([A (Z), if (B (Z) \leq D, B (Z), D))) \in ℝ$
19	12 17 18	syl2anc	$⊢ φ \to vol ([A (Z), if (B (Z) \leq D, B (Z), D))) \in ℝ$
20		difssd	$⊢ φ \to X ∖ \{Z\} \subseteq X$
21		ssfi	$⊢ (X \in Fin \land X ∖ \{Z\} \subseteq X) \to X ∖ \{Z\} \in Fin$
22	2 20 21	syl2anc	$⊢ φ \to X ∖ \{Z\} \in Fin$
23		eldifi	$⊢ k \in (X ∖ \{Z\}) \to k \in X$
24	23	adantl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to k \in X$
25	9	ffvelcdmda	$⊢ (φ \land k \in X) \to A (k) \in ℝ$
26	10	ffvelcdmda	$⊢ (φ \land k \in X) \to B (k) \in ℝ$
27		volicore	$⊢ (A (k) \in ℝ \land B (k) \in ℝ) \to vol ([A (k), B (k))) \in ℝ$
28	25 26 27	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), B (k))) \in ℝ$
29	24 28	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to vol ([A (k), B (k))) \in ℝ$
30	22 29	fprodrecl	$⊢ φ \to \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))) \in ℝ$
31		nfv	$⊢ Ⅎ k φ$
32	24 25	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to A (k) \in ℝ$
33	24 26	syldan	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B (k) \in ℝ$
34	33	rexrd	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B (k) \in ℝ^{*}$
35		icombl	$⊢ (A (k) \in ℝ \land B (k) \in ℝ^{*}) \to [A (k), B (k)) \in dom vol$
36	32 34 35	syl2anc	$⊢ (φ \land k \in (X ∖ \{Z\})) \to [A (k), B (k)) \in dom vol$
37		volge0	$⊢ [A (k), B (k)) \in dom vol \to 0 \leq vol ([A (k), B (k)))$
38	36 37	syl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to 0 \leq vol ([A (k), B (k)))$
39	31 22 29 38	fprodge0	$⊢ φ \to 0 \leq \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
40	14	rexrd	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \in ℝ^{*}$
41		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$
42	12 40 41	syl2anc	$⊢ φ \to [A (Z), if (B (Z) \leq C, B (Z), C)) \in dom vol$
43	17	rexrd	$⊢ φ \to if (B (Z) \leq D, B (Z), D) \in ℝ^{*}$
44		icombl	$⊢ (A (Z) \in ℝ \land if (B (Z) \leq D, B (Z), D) \in ℝ^{*}) \to [A (Z), if (B (Z) \leq D, B (Z), D)) \in dom vol$
45	12 43 44	syl2anc	$⊢ φ \to [A (Z), if (B (Z) \leq D, B (Z), D)) \in dom vol$
46	12	rexrd	$⊢ φ \to A (Z) \in ℝ^{*}$
47	12	leidd	$⊢ φ \to A (Z) \leq A (Z)$
48	13	leidd	$⊢ φ \to B (Z) \leq B (Z)$
49	48	adantr	$⊢ (φ \land B (Z) \leq C) \to B (Z) \leq B (Z)$
50		iftrue	$⊢ B (Z) \leq C \to if (B (Z) \leq C, B (Z), C) = B (Z)$
51	50	adantl	$⊢ (φ \land B (Z) \leq C) \to if (B (Z) \leq C, B (Z), C) = B (Z)$
52	13	adantr	$⊢ (φ \land B (Z) \leq C) \to B (Z) \in ℝ$
53	5	adantr	$⊢ (φ \land B (Z) \leq C) \to C \in ℝ$
54	6	adantr	$⊢ (φ \land B (Z) \leq C) \to D \in ℝ$
55		simpr	$⊢ (φ \land B (Z) \leq C) \to B (Z) \leq C$
56	7	adantr	$⊢ (φ \land B (Z) \leq C) \to C \leq D$
57	52 53 54 55 56	letrd	$⊢ (φ \land B (Z) \leq C) \to B (Z) \leq D$
58	57	iftrued	$⊢ (φ \land B (Z) \leq C) \to if (B (Z) \leq D, B (Z), D) = B (Z)$
59	51 58	breq12d	$⊢ (φ \land B (Z) \leq C) \to (if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D) \leftrightarrow B (Z) \leq B (Z))$
60	49 59	mpbird	$⊢ (φ \land B (Z) \leq C) \to if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D)$
61		simpl	$⊢ (φ \land \neg B (Z) \leq C) \to φ$
62		simpr	$⊢ (φ \land \neg B (Z) \leq C) \to \neg B (Z) \leq C$
63	61 5	syl	$⊢ (φ \land \neg B (Z) \leq C) \to C \in ℝ$
64	61 13	syl	$⊢ (φ \land \neg B (Z) \leq C) \to B (Z) \in ℝ$
65	63 64	ltnled	$⊢ (φ \land \neg B (Z) \leq C) \to (C < B (Z) \leftrightarrow \neg B (Z) \leq C)$
66	62 65	mpbird	$⊢ (φ \land \neg B (Z) \leq C) \to C < B (Z)$
67	5	adantr	$⊢ (φ \land C < B (Z)) \to C \in ℝ$
68	13	adantr	$⊢ (φ \land C < B (Z)) \to B (Z) \in ℝ$
69		simpr	$⊢ (φ \land C < B (Z)) \to C < B (Z)$
70	67 68 69	ltled	$⊢ (φ \land C < B (Z)) \to C \leq B (Z)$
71	70	adantr	$⊢ ((φ \land C < B (Z)) \land B (Z) \leq D) \to C \leq B (Z)$
72		iftrue	$⊢ B (Z) \leq D \to if (B (Z) \leq D, B (Z), D) = B (Z)$
73	72	eqcomd	$⊢ B (Z) \leq D \to B (Z) = if (B (Z) \leq D, B (Z), D)$
74	73	adantl	$⊢ ((φ \land C < B (Z)) \land B (Z) \leq D) \to B (Z) = if (B (Z) \leq D, B (Z), D)$
75	71 74	breqtrd	$⊢ ((φ \land C < B (Z)) \land B (Z) \leq D) \to C \leq if (B (Z) \leq D, B (Z), D)$
76	7	ad2antrr	$⊢ ((φ \land C < B (Z)) \land \neg B (Z) \leq D) \to C \leq D$
77		iffalse	$⊢ \neg B (Z) \leq D \to if (B (Z) \leq D, B (Z), D) = D$
78	77	eqcomd	$⊢ \neg B (Z) \leq D \to D = if (B (Z) \leq D, B (Z), D)$
79	78	adantl	$⊢ ((φ \land C < B (Z)) \land \neg B (Z) \leq D) \to D = if (B (Z) \leq D, B (Z), D)$
80	76 79	breqtrd	$⊢ ((φ \land C < B (Z)) \land \neg B (Z) \leq D) \to C \leq if (B (Z) \leq D, B (Z), D)$
81	75 80	pm2.61dan	$⊢ (φ \land C < B (Z)) \to C \leq if (B (Z) \leq D, B (Z), D)$
82	61 66 81	syl2anc	$⊢ (φ \land \neg B (Z) \leq C) \to C \leq if (B (Z) \leq D, B (Z), D)$
83		iffalse	$⊢ \neg B (Z) \leq C \to if (B (Z) \leq C, B (Z), C) = C$
84	83	adantl	$⊢ (φ \land \neg B (Z) \leq C) \to if (B (Z) \leq C, B (Z), C) = C$
85	84	breq1d	$⊢ (φ \land \neg B (Z) \leq C) \to (if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D) \leftrightarrow C \leq if (B (Z) \leq D, B (Z), D))$
86	82 85	mpbird	$⊢ (φ \land \neg B (Z) \leq C) \to if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D)$
87	60 86	pm2.61dan	$⊢ φ \to if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D)$
88		icossico	$⊢ ((A (Z) \in ℝ^{} \land if (B (Z) \leq D, B (Z), D) \in ℝ^{}) \land (A (Z) \leq A (Z) \land if (B (Z) \leq C, B (Z), C) \leq if (B (Z) \leq D, B (Z), D))) \to [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), if (B (Z) \leq D, B (Z), D))$
89	46 43 47 87 88	syl22anc	$⊢ φ \to [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), if (B (Z) \leq D, B (Z), D))$
90		volss	$⊢ ([A (Z), if (B (Z) \leq C, B (Z), C)) \in dom vol \land [A (Z), if (B (Z) \leq D, B (Z), D)) \in dom vol \land [A (Z), if (B (Z) \leq C, B (Z), C)) \subseteq [A (Z), if (B (Z) \leq D, B (Z), D))) \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \leq vol ([A (Z), if (B (Z) \leq D, B (Z), D)))$
91	42 45 89 90	syl3anc	$⊢ φ \to vol ([A (Z), if (B (Z) \leq C, B (Z), C))) \leq vol ([A (Z), if (B (Z) \leq D, B (Z), D)))$
92	16 19 30 39 91	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), if (B (Z) \leq D, B (Z), D))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
93	11	ne0d	$⊢ φ \to X \neq \emptyset$
94	8 5 2 10	hsphoif	$⊢ φ \to H (C) (B) : X ⟶ ℝ$
95	1 2 93 9 94	hoidmvn0val	$⊢ φ \to A L (X) H (C) (B) = \prod_{k \in X} vol ([A (k), H (C) (B) (k)))$
96	94	ffvelcdmda	$⊢ (φ \land k \in X) \to H (C) (B) (k) \in ℝ$
97		volicore	$⊢ (A (k) \in ℝ \land H (C) (B) (k) \in ℝ) \to vol ([A (k), H (C) (B) (k))) \in ℝ$
98	25 96 97	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), H (C) (B) (k))) \in ℝ$
99	98	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), H (C) (B) (k))) \in ℂ$
100		fveq2	$⊢ k = Z \to A (k) = A (Z)$
101		fveq2	$⊢ k = Z \to H (C) (B) (k) = H (C) (B) (Z)$
102	100 101	oveq12d	$⊢ k = Z \to [A (k), H (C) (B) (k)) = [A (Z), H (C) (B) (Z))$
103	102	fveq2d	$⊢ k = Z \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), H (C) (B) (Z)))$
104	103	adantl	$⊢ (φ \land k = Z) \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), H (C) (B) (Z)))$
105	8 5 2 10 11	hsphoival	$⊢ φ \to H (C) (B) (Z) = if (Z \in Y, B (Z), if (B (Z) \leq C, B (Z), C))$
106	3	eldifbd	$⊢ φ \to \neg Z \in Y$
107	106	iffalsed	$⊢ φ \to if (Z \in Y, B (Z), if (B (Z) \leq C, B (Z), C)) = if (B (Z) \leq C, B (Z), C)$
108	105 107	eqtrd	$⊢ φ \to H (C) (B) (Z) = if (B (Z) \leq C, B (Z), C)$
109	108	oveq2d	$⊢ φ \to [A (Z), H (C) (B) (Z)) = [A (Z), if (B (Z) \leq C, B (Z), C))$
110	109	fveq2d	$⊢ φ \to vol ([A (Z), H (C) (B) (Z))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
111	110	adantr	$⊢ (φ \land k = Z) \to vol ([A (Z), H (C) (B) (Z))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
112	104 111	eqtrd	$⊢ (φ \land k = Z) \to vol ([A (k), H (C) (B) (k))) = vol ([A (Z), if (B (Z) \leq C, B (Z), C)))$
113	2 99 11 112	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)))$
114	5	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to C \in ℝ$
115	2	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to X \in Fin$
116	10	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to B : X ⟶ ℝ$
117	8 114 115 116 24	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))$
118	23 4	eleqtrdi	$⊢ k \in (X ∖ \{Z\}) \to k \in (Y \cup \{Z\})$
119		eldifn	$⊢ k \in (X ∖ \{Z\}) \to \neg k \in \{Z\}$
120		elunnel2	$⊢ (k \in (Y \cup \{Z\}) \land \neg k \in \{Z\}) \to k \in Y$
121	118 119 120	syl2anc	$⊢ k \in (X ∖ \{Z\}) \to k \in Y$
122	121	adantl	$⊢ (φ \land k \in (X ∖ \{Z\})) \to k \in Y$
123	122	iftrued	$⊢ (φ \land k \in (X ∖ \{Z\})) \to if (k \in Y, B (k), if (B (k) \leq C, B (k), C)) = B (k)$
124	117 123	eqtrd	$⊢ (φ \land k \in (X ∖ \{Z\})) \to H (C) (B) (k) = B (k)$
125	124	oveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to [A (k), H (C) (B) (k)) = [A (k), B (k))$
126	125	fveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to vol ([A (k), H (C) (B) (k))) = vol ([A (k), B (k)))$
127	126	prodeq2dv	$⊢ φ \to \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (C) (B) (k))) = \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
128	127	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)))$
129	95 113 128	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)))$
130	8 6 2 10	hsphoif	$⊢ φ \to H (D) (B) : X ⟶ ℝ$
131	1 2 93 9 130	hoidmvn0val	$⊢ φ \to A L (X) H (D) (B) = \prod_{k \in X} vol ([A (k), H (D) (B) (k)))$
132	130	ffvelcdmda	$⊢ (φ \land k \in X) \to H (D) (B) (k) \in ℝ$
133		volicore	$⊢ (A (k) \in ℝ \land H (D) (B) (k) \in ℝ) \to vol ([A (k), H (D) (B) (k))) \in ℝ$
134	25 132 133	syl2anc	$⊢ (φ \land k \in X) \to vol ([A (k), H (D) (B) (k))) \in ℝ$
135	134	recnd	$⊢ (φ \land k \in X) \to vol ([A (k), H (D) (B) (k))) \in ℂ$
136		fveq2	$⊢ k = Z \to H (D) (B) (k) = H (D) (B) (Z)$
137	100 136	oveq12d	$⊢ k = Z \to [A (k), H (D) (B) (k)) = [A (Z), H (D) (B) (Z))$
138	137	fveq2d	$⊢ k = Z \to vol ([A (k), H (D) (B) (k))) = vol ([A (Z), H (D) (B) (Z)))$
139	138	adantl	$⊢ (φ \land k = Z) \to vol ([A (k), H (D) (B) (k))) = vol ([A (Z), H (D) (B) (Z)))$
140	2 135 11 139	fprodsplit1	$⊢ φ \to \prod_{k \in X} vol ([A (k), H (D) (B) (k))) = vol ([A (Z), H (D) (B) (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (D) (B) (k)))$
141	8 6 2 10 11	hsphoival	$⊢ φ \to H (D) (B) (Z) = if (Z \in Y, B (Z), if (B (Z) \leq D, B (Z), D))$
142	106	iffalsed	$⊢ φ \to if (Z \in Y, B (Z), if (B (Z) \leq D, B (Z), D)) = if (B (Z) \leq D, B (Z), D)$
143	141 142	eqtrd	$⊢ φ \to H (D) (B) (Z) = if (B (Z) \leq D, B (Z), D)$
144	143	oveq2d	$⊢ φ \to [A (Z), H (D) (B) (Z)) = [A (Z), if (B (Z) \leq D, B (Z), D))$
145	144	fveq2d	$⊢ φ \to vol ([A (Z), H (D) (B) (Z))) = vol ([A (Z), if (B (Z) \leq D, B (Z), D)))$
146	6	adantr	$⊢ (φ \land k \in (X ∖ \{Z\})) \to D \in ℝ$
147	8 146 115 116 24	hsphoival	$⊢ (φ \land k \in (X ∖ \{Z\})) \to H (D) (B) (k) = if (k \in Y, B (k), if (B (k) \leq D, B (k), D))$
148	122	iftrued	$⊢ (φ \land k \in (X ∖ \{Z\})) \to if (k \in Y, B (k), if (B (k) \leq D, B (k), D)) = B (k)$
149	147 148	eqtrd	$⊢ (φ \land k \in (X ∖ \{Z\})) \to H (D) (B) (k) = B (k)$
150	149	oveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to [A (k), H (D) (B) (k)) = [A (k), B (k))$
151	150	fveq2d	$⊢ (φ \land k \in (X ∖ \{Z\})) \to vol ([A (k), H (D) (B) (k))) = vol ([A (k), B (k)))$
152	151	prodeq2dv	$⊢ φ \to \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (D) (B) (k))) = \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
153	145 152	oveq12d	$⊢ φ \to vol ([A (Z), H (D) (B) (Z))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), H (D) (B) (k))) = vol ([A (Z), if (B (Z) \leq D, B (Z), D))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
154	131 140 153	3eqtrd	$⊢ φ \to A L (X) H (D) (B) = vol ([A (Z), if (B (Z) \leq D, B (Z), D))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k)))$
155	129 154	breq12d	$⊢ φ \to (A L (X) H (C) (B) \leq A L (X) H (D) (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), if (B (Z) \leq D, B (Z), D))) \prod_{k \in X ∖ \{Z\}} vol ([A (k), B (k))))$
156	92 155	mpbird	$⊢ φ \to A L (X) H (C) (B) \leq A L (X) H (D) (B)$

Metamath Proof Explorer

Theorem hsphoidmvle2

Proof