hspmbllem1

Description: Any half-space of the n-dimensional Real numbers is Lebesgue measurable. This is Step (a) of Lemma 115F of Fremlin1 p. 31. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hspmbllem1.x	$⊢ φ \to X \in Fin$
	hspmbllem1.k	$⊢ φ \to K \in X$
	hspmbllem1.y	$⊢ φ \to Y \in ℝ$
	hspmbllem1.a	$⊢ φ \to A : X ⟶ ℝ$
	hspmbllem1.b	$⊢ φ \to B : X ⟶ ℝ$
	hspmbllem1.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
	hspmbllem1.t	$⊢ T = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
	hspmbllem1.s	$⊢ S = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
Assertion	hspmbllem1	$⊢ φ \to A L (X) B = (A L (X) T (Y) (B)) +_{𝑒} (S (Y) (A) L (X) B)$

Proof

Step	Hyp	Ref	Expression
1		hspmbllem1.x	$⊢ φ \to X \in Fin$
2		hspmbllem1.k	$⊢ φ \to K \in X$
3		hspmbllem1.y	$⊢ φ \to Y \in ℝ$
4		hspmbllem1.a	$⊢ φ \to A : X ⟶ ℝ$
5		hspmbllem1.b	$⊢ φ \to B : X ⟶ ℝ$
6		hspmbllem1.l	$⊢ L = (x \in Fin ⟼ (a \in (ℝ^{x}), b \in (ℝ^{x}) ⟼ if (x = \emptyset, 0, \prod_{k \in x} vol ([a (k), b (k))))))$
7		hspmbllem1.t	$⊢ T = (y \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h \in (X ∖ \{K\}), c (h), if (c (h) \leq y, c (h), y)))))$
8		hspmbllem1.s	$⊢ S = (x \in ℝ ⟼ (c \in (ℝ^{X}) ⟼ (h \in X ⟼ if (h = K, if (x \leq c (h), c (h), x), c (h)))))$
9		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
10	7 3 1 5	hsphoif	$⊢ φ \to T (Y) (B) : X ⟶ ℝ$
11	6 1 4 10	hoidmvcl	$⊢ φ \to A L (X) T (Y) (B) \in [0, +∞)$
12	9 11	sselid	$⊢ φ \to A L (X) T (Y) (B) \in ℝ$
13	8 3 1 4	hoidifhspf	$⊢ φ \to S (Y) (A) : X ⟶ ℝ$
14	6 1 13 5	hoidmvcl	$⊢ φ \to S (Y) (A) L (X) B \in [0, +∞)$
15	9 14	sselid	$⊢ φ \to S (Y) (A) L (X) B \in ℝ$
16	12 15	rexaddd	$⊢ φ \to (A L (X) T (Y) (B)) +_{𝑒} (S (Y) (A) L (X) B) = (A L (X) T (Y) (B)) + (S (Y) (A) L (X) B)$
17	2	ne0d	$⊢ φ \to X \neq \emptyset$
18	6 1 17 4 10	hoidmvn0val	$⊢ φ \to A L (X) T (Y) (B) = \prod_{k \in X} vol ([A (k), T (Y) (B) (k)))$
19	6 1 17 13 5	hoidmvn0val	$⊢ φ \to S (Y) (A) L (X) B = \prod_{k \in X} vol ([S (Y) (A) (k), B (k)))$
20	18 19	oveq12d	$⊢ φ \to (A L (X) T (Y) (B)) + (S (Y) (A) L (X) B) = \prod_{k \in X} vol ([A (k), T (Y) (B) (k))) + \prod_{k \in X} vol ([S (Y) (A) (k), B (k)))$
21		uncom	$⊢ (X ∖ \{K\}) \cup \{K\} = \{K\} \cup (X ∖ \{K\})$
22	21	a1i	$⊢ φ \to (X ∖ \{K\}) \cup \{K\} = \{K\} \cup (X ∖ \{K\})$
23	2	snssd	$⊢ φ \to \{K\} \subseteq X$
24		undif	$⊢ \{K\} \subseteq X \leftrightarrow \{K\} \cup (X ∖ \{K\}) = X$
25	23 24	sylib	$⊢ φ \to \{K\} \cup (X ∖ \{K\}) = X$
26	22 25	eqtrd	$⊢ φ \to (X ∖ \{K\}) \cup \{K\} = X$
27	26	eqcomd	$⊢ φ \to X = (X ∖ \{K\}) \cup \{K\}$
28	27	prodeq1d	$⊢ φ \to \prod_{k \in X} vol ([A (k), T (Y) (B) (k))) = \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([A (k), T (Y) (B) (k)))$
29		nfv	$⊢ Ⅎ k φ$
30		nfcv	$⊢ \underline{Ⅎ} k vol ([A (K), T (Y) (B) (K)))$
31		difssd	$⊢ φ \to X ∖ \{K\} \subseteq X$
32	1 31	ssfid	$⊢ φ \to X ∖ \{K\} \in Fin$
33		neldifsnd	$⊢ φ \to \neg K \in (X ∖ \{K\})$
34	4	adantr	$⊢ (φ \land k \in (X ∖ \{K\})) \to A : X ⟶ ℝ$
35	31	sselda	$⊢ (φ \land k \in (X ∖ \{K\})) \to k \in X$
36	34 35	ffvelcdmd	$⊢ (φ \land k \in (X ∖ \{K\})) \to A (k) \in ℝ$
37	3	adantr	$⊢ (φ \land k \in (X ∖ \{K\})) \to Y \in ℝ$
38	1	adantr	$⊢ (φ \land k \in (X ∖ \{K\})) \to X \in Fin$
39	5	adantr	$⊢ (φ \land k \in (X ∖ \{K\})) \to B : X ⟶ ℝ$
40	7 37 38 39	hsphoif	$⊢ (φ \land k \in (X ∖ \{K\})) \to T (Y) (B) : X ⟶ ℝ$
41	40 35	ffvelcdmd	$⊢ (φ \land k \in (X ∖ \{K\})) \to T (Y) (B) (k) \in ℝ$
42		volicore	$⊢ (A (k) \in ℝ \land T (Y) (B) (k) \in ℝ) \to vol ([A (k), T (Y) (B) (k))) \in ℝ$
43	36 41 42	syl2anc	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([A (k), T (Y) (B) (k))) \in ℝ$
44	43	recnd	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([A (k), T (Y) (B) (k))) \in ℂ$
45		fveq2	$⊢ k = K \to A (k) = A (K)$
46		fveq2	$⊢ k = K \to T (Y) (B) (k) = T (Y) (B) (K)$
47	45 46	oveq12d	$⊢ k = K \to [A (k), T (Y) (B) (k)) = [A (K), T (Y) (B) (K))$
48	47	fveq2d	$⊢ k = K \to vol ([A (k), T (Y) (B) (k))) = vol ([A (K), T (Y) (B) (K)))$
49	4 2	ffvelcdmd	$⊢ φ \to A (K) \in ℝ$
50	10 2	ffvelcdmd	$⊢ φ \to T (Y) (B) (K) \in ℝ$
51		volicore	$⊢ (A (K) \in ℝ \land T (Y) (B) (K) \in ℝ) \to vol ([A (K), T (Y) (B) (K))) \in ℝ$
52	49 50 51	syl2anc	$⊢ φ \to vol ([A (K), T (Y) (B) (K))) \in ℝ$
53	52	recnd	$⊢ φ \to vol ([A (K), T (Y) (B) (K))) \in ℂ$
54	29 30 32 2 33 44 48 53	fprodsplitsn	$⊢ φ \to \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([A (k), T (Y) (B) (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), T (Y) (B) (k))) vol ([A (K), T (Y) (B) (K)))$
55	7 37 38 39 35	hsphoival	$⊢ (φ \land k \in (X ∖ \{K\})) \to T (Y) (B) (k) = if (k \in (X ∖ \{K\}), B (k), if (B (k) \leq Y, B (k), Y))$
56		iftrue	$⊢ k \in (X ∖ \{K\}) \to if (k \in (X ∖ \{K\}), B (k), if (B (k) \leq Y, B (k), Y)) = B (k)$
57	56	adantl	$⊢ (φ \land k \in (X ∖ \{K\})) \to if (k \in (X ∖ \{K\}), B (k), if (B (k) \leq Y, B (k), Y)) = B (k)$
58	55 57	eqtrd	$⊢ (φ \land k \in (X ∖ \{K\})) \to T (Y) (B) (k) = B (k)$
59	58	oveq2d	$⊢ (φ \land k \in (X ∖ \{K\})) \to [A (k), T (Y) (B) (k)) = [A (k), B (k))$
60	59	fveq2d	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([A (k), T (Y) (B) (k))) = vol ([A (k), B (k)))$
61	60	prodeq2dv	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), T (Y) (B) (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k)))$
62	61	oveq1d	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), T (Y) (B) (k))) vol ([A (K), T (Y) (B) (K))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), T (Y) (B) (K)))$
63	28 54 62	3eqtrd	$⊢ φ \to \prod_{k \in X} vol ([A (k), T (Y) (B) (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), T (Y) (B) (K)))$
64	27	prodeq1d	$⊢ φ \to \prod_{k \in X} vol ([S (Y) (A) (k), B (k))) = \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([S (Y) (A) (k), B (k)))$
65		nfcv	$⊢ \underline{Ⅎ} k vol ([S (Y) (A) (K), B (K)))$
66	13	adantr	$⊢ (φ \land k \in (X ∖ \{K\})) \to S (Y) (A) : X ⟶ ℝ$
67	66 35	ffvelcdmd	$⊢ (φ \land k \in (X ∖ \{K\})) \to S (Y) (A) (k) \in ℝ$
68	58 41	eqeltrrd	$⊢ (φ \land k \in (X ∖ \{K\})) \to B (k) \in ℝ$
69		volicore	$⊢ (S (Y) (A) (k) \in ℝ \land B (k) \in ℝ) \to vol ([S (Y) (A) (k), B (k))) \in ℝ$
70	67 68 69	syl2anc	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([S (Y) (A) (k), B (k))) \in ℝ$
71	70	recnd	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([S (Y) (A) (k), B (k))) \in ℂ$
72		fveq2	$⊢ k = K \to S (Y) (A) (k) = S (Y) (A) (K)$
73		fveq2	$⊢ k = K \to B (k) = B (K)$
74	72 73	oveq12d	$⊢ k = K \to [S (Y) (A) (k), B (k)) = [S (Y) (A) (K), B (K))$
75	74	fveq2d	$⊢ k = K \to vol ([S (Y) (A) (k), B (k))) = vol ([S (Y) (A) (K), B (K)))$
76	13 2	ffvelcdmd	$⊢ φ \to S (Y) (A) (K) \in ℝ$
77	5 2	ffvelcdmd	$⊢ φ \to B (K) \in ℝ$
78		volicore	$⊢ (S (Y) (A) (K) \in ℝ \land B (K) \in ℝ) \to vol ([S (Y) (A) (K), B (K))) \in ℝ$
79	76 77 78	syl2anc	$⊢ φ \to vol ([S (Y) (A) (K), B (K))) \in ℝ$
80	79	recnd	$⊢ φ \to vol ([S (Y) (A) (K), B (K))) \in ℂ$
81	29 65 32 2 33 71 75 80	fprodsplitsn	$⊢ φ \to \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([S (Y) (A) (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([S (Y) (A) (k), B (k))) vol ([S (Y) (A) (K), B (K)))$
82	8 37 38 34 35	hoidifhspval3	$⊢ (φ \land k \in (X ∖ \{K\})) \to S (Y) (A) (k) = if (k = K, if (Y \leq A (k), A (k), Y), A (k))$
83		eldifsni	$⊢ k \in (X ∖ \{K\}) \to k \neq K$
84		neneq	$⊢ k \neq K \to \neg k = K$
85	83 84	syl	$⊢ k \in (X ∖ \{K\}) \to \neg k = K$
86	85	iffalsed	$⊢ k \in (X ∖ \{K\}) \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = A (k)$
87	86	adantl	$⊢ (φ \land k \in (X ∖ \{K\})) \to if (k = K, if (Y \leq A (k), A (k), Y), A (k)) = A (k)$
88	82 87	eqtrd	$⊢ (φ \land k \in (X ∖ \{K\})) \to S (Y) (A) (k) = A (k)$
89	88	fvoveq1d	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([S (Y) (A) (k), B (k))) = vol ([A (k), B (k)))$
90	89	prodeq2dv	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([S (Y) (A) (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k)))$
91	90	oveq1d	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([S (Y) (A) (k), B (k))) vol ([S (Y) (A) (K), B (K))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([S (Y) (A) (K), B (K)))$
92	64 81 91	3eqtrd	$⊢ φ \to \prod_{k \in X} vol ([S (Y) (A) (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([S (Y) (A) (K), B (K)))$
93	63 92	oveq12d	$⊢ φ \to \prod_{k \in X} vol ([A (k), T (Y) (B) (k))) + \prod_{k \in X} vol ([S (Y) (A) (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), T (Y) (B) (K))) + \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([S (Y) (A) (K), B (K)))$
94	27	prodeq1d	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([A (k), B (k)))$
95		nfcv	$⊢ \underline{Ⅎ} k vol ([A (K), B (K)))$
96	60 44	eqeltrrd	$⊢ (φ \land k \in (X ∖ \{K\})) \to vol ([A (k), B (k))) \in ℂ$
97	45 73	oveq12d	$⊢ k = K \to [A (k), B (k)) = [A (K), B (K))$
98	97	fveq2d	$⊢ k = K \to vol ([A (k), B (k))) = vol ([A (K), B (K)))$
99		volicore	$⊢ (A (K) \in ℝ \land B (K) \in ℝ) \to vol ([A (K), B (K))) \in ℝ$
100	49 77 99	syl2anc	$⊢ φ \to vol ([A (K), B (K))) \in ℝ$
101	100	recnd	$⊢ φ \to vol ([A (K), B (K))) \in ℂ$
102	29 95 32 2 33 96 98 101	fprodsplitsn	$⊢ φ \to \prod_{k \in (X ∖ \{K\}) \cup \{K\}} vol ([A (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), B (K)))$
103	94 102	eqtrd	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), B (K)))$
104	7 3 1 5 2	hsphoival	$⊢ φ \to T (Y) (B) (K) = if (K \in (X ∖ \{K\}), B (K), if (B (K) \leq Y, B (K), Y))$
105	33	iffalsed	$⊢ φ \to if (K \in (X ∖ \{K\}), B (K), if (B (K) \leq Y, B (K), Y)) = if (B (K) \leq Y, B (K), Y)$
106	104 105	eqtrd	$⊢ φ \to T (Y) (B) (K) = if (B (K) \leq Y, B (K), Y)$
107	106	oveq2d	$⊢ φ \to [A (K), T (Y) (B) (K)) = [A (K), if (B (K) \leq Y, B (K), Y))$
108	107	fveq2d	$⊢ φ \to vol ([A (K), T (Y) (B) (K))) = vol ([A (K), if (B (K) \leq Y, B (K), Y)))$
109	8 3 1 4 2	hoidifhspval3	$⊢ φ \to S (Y) (A) (K) = if (K = K, if (Y \leq A (K), A (K), Y), A (K))$
110		eqid	$⊢ K = K$
111	110	iftruei	$⊢ if (K = K, if (Y \leq A (K), A (K), Y), A (K)) = if (Y \leq A (K), A (K), Y)$
112	111	a1i	$⊢ φ \to if (K = K, if (Y \leq A (K), A (K), Y), A (K)) = if (Y \leq A (K), A (K), Y)$
113	109 112	eqtrd	$⊢ φ \to S (Y) (A) (K) = if (Y \leq A (K), A (K), Y)$
114	113	fvoveq1d	$⊢ φ \to vol ([S (Y) (A) (K), B (K))) = vol ([if (Y \leq A (K), A (K), Y), B (K)))$
115	108 114	oveq12d	$⊢ φ \to vol ([A (K), T (Y) (B) (K))) + vol ([S (Y) (A) (K), B (K))) = vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K)))$
116		iftrue	$⊢ B (K) \leq Y \to if (B (K) \leq Y, B (K), Y) = B (K)$
117	116	oveq2d	$⊢ B (K) \leq Y \to [A (K), if (B (K) \leq Y, B (K), Y)) = [A (K), B (K))$
118	117	fveq2d	$⊢ B (K) \leq Y \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) = vol ([A (K), B (K)))$
119	118	oveq1d	$⊢ B (K) \leq Y \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K))) + vol ([if (Y \leq A (K), A (K), Y), B (K)))$
120	119	adantl	$⊢ (φ \land B (K) \leq Y) \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K))) + vol ([if (Y \leq A (K), A (K), Y), B (K)))$
121		iftrue	$⊢ Y \leq A (K) \to if (Y \leq A (K), A (K), Y) = A (K)$
122	121	oveq1d	$⊢ Y \leq A (K) \to [if (Y \leq A (K), A (K), Y), B (K)) = [A (K), B (K))$
123	122	adantl	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to [if (Y \leq A (K), A (K), Y), B (K)) = [A (K), B (K))$
124	77	ad2antrr	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to B (K) \in ℝ$
125	3	ad2antrr	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to Y \in ℝ$
126	49	ad2antrr	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to A (K) \in ℝ$
127		simplr	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to B (K) \leq Y$
128		simpr	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to Y \leq A (K)$
129	124 125 126 127 128	letrd	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to B (K) \leq A (K)$
130	126	rexrd	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to A (K) \in ℝ^{*}$
131	124	rexrd	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to B (K) \in ℝ^{*}$
132		ico0	$⊢ (A (K) \in ℝ^{} \land B (K) \in ℝ^{}) \to ([A (K), B (K)) = \emptyset \leftrightarrow B (K) \leq A (K))$
133	130 131 132	syl2anc	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to ([A (K), B (K)) = \emptyset \leftrightarrow B (K) \leq A (K))$
134	129 133	mpbird	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to [A (K), B (K)) = \emptyset$
135	123 134	eqtrd	$⊢ ((φ \land B (K) \leq Y) \land Y \leq A (K)) \to [if (Y \leq A (K), A (K), Y), B (K)) = \emptyset$
136		iffalse	$⊢ \neg Y \leq A (K) \to if (Y \leq A (K), A (K), Y) = Y$
137	136	oveq1d	$⊢ \neg Y \leq A (K) \to [if (Y \leq A (K), A (K), Y), B (K)) = [Y, B (K))$
138	137	adantl	$⊢ ((φ \land B (K) \leq Y) \land \neg Y \leq A (K)) \to [if (Y \leq A (K), A (K), Y), B (K)) = [Y, B (K))$
139		simpr	$⊢ (φ \land B (K) \leq Y) \to B (K) \leq Y$
140	3	rexrd	$⊢ φ \to Y \in ℝ^{*}$
141	140	adantr	$⊢ (φ \land B (K) \leq Y) \to Y \in ℝ^{*}$
142	77	rexrd	$⊢ φ \to B (K) \in ℝ^{*}$
143	142	adantr	$⊢ (φ \land B (K) \leq Y) \to B (K) \in ℝ^{*}$
144		ico0	$⊢ (Y \in ℝ^{} \land B (K) \in ℝ^{}) \to ([Y, B (K)) = \emptyset \leftrightarrow B (K) \leq Y)$
145	141 143 144	syl2anc	$⊢ (φ \land B (K) \leq Y) \to ([Y, B (K)) = \emptyset \leftrightarrow B (K) \leq Y)$
146	139 145	mpbird	$⊢ (φ \land B (K) \leq Y) \to [Y, B (K)) = \emptyset$
147	146	adantr	$⊢ ((φ \land B (K) \leq Y) \land \neg Y \leq A (K)) \to [Y, B (K)) = \emptyset$
148	138 147	eqtrd	$⊢ ((φ \land B (K) \leq Y) \land \neg Y \leq A (K)) \to [if (Y \leq A (K), A (K), Y), B (K)) = \emptyset$
149	135 148	pm2.61dan	$⊢ (φ \land B (K) \leq Y) \to [if (Y \leq A (K), A (K), Y), B (K)) = \emptyset$
150	149	fveq2d	$⊢ (φ \land B (K) \leq Y) \to vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol (\emptyset)$
151		vol0	$⊢ vol (\emptyset) = 0$
152	151	a1i	$⊢ (φ \land B (K) \leq Y) \to vol (\emptyset) = 0$
153	150 152	eqtrd	$⊢ (φ \land B (K) \leq Y) \to vol ([if (Y \leq A (K), A (K), Y), B (K))) = 0$
154	153	oveq2d	$⊢ (φ \land B (K) \leq Y) \to vol ([A (K), B (K))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K))) + 0$
155	101	addridd	$⊢ φ \to vol ([A (K), B (K))) + 0 = vol ([A (K), B (K)))$
156	155	adantr	$⊢ (φ \land B (K) \leq Y) \to vol ([A (K), B (K))) + 0 = vol ([A (K), B (K)))$
157	120 154 156	3eqtrd	$⊢ (φ \land B (K) \leq Y) \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
158		iffalse	$⊢ \neg B (K) \leq Y \to if (B (K) \leq Y, B (K), Y) = Y$
159	158	oveq2d	$⊢ \neg B (K) \leq Y \to [A (K), if (B (K) \leq Y, B (K), Y)) = [A (K), Y)$
160	159	fveq2d	$⊢ \neg B (K) \leq Y \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) = vol ([A (K), Y))$
161	160	adantl	$⊢ (φ \land \neg B (K) \leq Y) \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) = vol ([A (K), Y))$
162	161	oveq1d	$⊢ (φ \land \neg B (K) \leq Y) \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K)))$
163		simpl	$⊢ (φ \land \neg B (K) \leq Y) \to φ$
164		simpr	$⊢ (φ \land \neg B (K) \leq Y) \to \neg B (K) \leq Y$
165	163 3	syl	$⊢ (φ \land \neg B (K) \leq Y) \to Y \in ℝ$
166	163 77	syl	$⊢ (φ \land \neg B (K) \leq Y) \to B (K) \in ℝ$
167	165 166	ltnled	$⊢ (φ \land \neg B (K) \leq Y) \to (Y < B (K) \leftrightarrow \neg B (K) \leq Y)$
168	164 167	mpbird	$⊢ (φ \land \neg B (K) \leq Y) \to Y < B (K)$
169	121	fvoveq1d	$⊢ Y \leq A (K) \to vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
170	169	oveq2d	$⊢ Y \leq A (K) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), Y)) + vol ([A (K), B (K)))$
171	170	adantl	$⊢ ((φ \land Y < B (K)) \land Y \leq A (K)) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), Y)) + vol ([A (K), B (K)))$
172		simpr	$⊢ (φ \land Y \leq A (K)) \to Y \leq A (K)$
173	49	rexrd	$⊢ φ \to A (K) \in ℝ^{*}$
174	173	adantr	$⊢ (φ \land Y \leq A (K)) \to A (K) \in ℝ^{*}$
175	140	adantr	$⊢ (φ \land Y \leq A (K)) \to Y \in ℝ^{*}$
176		ico0	$⊢ (A (K) \in ℝ^{} \land Y \in ℝ^{}) \to ([A (K), Y) = \emptyset \leftrightarrow Y \leq A (K))$
177	174 175 176	syl2anc	$⊢ (φ \land Y \leq A (K)) \to ([A (K), Y) = \emptyset \leftrightarrow Y \leq A (K))$
178	172 177	mpbird	$⊢ (φ \land Y \leq A (K)) \to [A (K), Y) = \emptyset$
179	178	fveq2d	$⊢ (φ \land Y \leq A (K)) \to vol ([A (K), Y)) = vol (\emptyset)$
180	151	a1i	$⊢ (φ \land Y \leq A (K)) \to vol (\emptyset) = 0$
181	179 180	eqtrd	$⊢ (φ \land Y \leq A (K)) \to vol ([A (K), Y)) = 0$
182	181	oveq1d	$⊢ (φ \land Y \leq A (K)) \to vol ([A (K), Y)) + vol ([A (K), B (K))) = 0 + vol ([A (K), B (K)))$
183	182	adantlr	$⊢ ((φ \land Y < B (K)) \land Y \leq A (K)) \to vol ([A (K), Y)) + vol ([A (K), B (K))) = 0 + vol ([A (K), B (K)))$
184	101	addlidd	$⊢ φ \to 0 + vol ([A (K), B (K))) = vol ([A (K), B (K)))$
185	184	ad2antrr	$⊢ ((φ \land Y < B (K)) \land Y \leq A (K)) \to 0 + vol ([A (K), B (K))) = vol ([A (K), B (K)))$
186	171 183 185	3eqtrd	$⊢ ((φ \land Y < B (K)) \land Y \leq A (K)) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
187	136	fvoveq1d	$⊢ \neg Y \leq A (K) \to vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([Y, B (K)))$
188	187	oveq2d	$⊢ \neg Y \leq A (K) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), Y)) + vol ([Y, B (K)))$
189	188	adantl	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), Y)) + vol ([Y, B (K)))$
190		simpl	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to (φ \land Y < B (K))$
191		simpr	$⊢ (φ \land \neg Y \leq A (K)) \to \neg Y \leq A (K)$
192	49	adantr	$⊢ (φ \land \neg Y \leq A (K)) \to A (K) \in ℝ$
193	3	adantr	$⊢ (φ \land \neg Y \leq A (K)) \to Y \in ℝ$
194	192 193	ltnled	$⊢ (φ \land \neg Y \leq A (K)) \to (A (K) < Y \leftrightarrow \neg Y \leq A (K))$
195	191 194	mpbird	$⊢ (φ \land \neg Y \leq A (K)) \to A (K) < Y$
196	195	adantlr	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to A (K) < Y$
197	49	adantr	$⊢ (φ \land A (K) < Y) \to A (K) \in ℝ$
198	3	adantr	$⊢ (φ \land A (K) < Y) \to Y \in ℝ$
199		volico	$⊢ (A (K) \in ℝ \land Y \in ℝ) \to vol ([A (K), Y)) = if (A (K) < Y, Y - A (K), 0)$
200	197 198 199	syl2anc	$⊢ (φ \land A (K) < Y) \to vol ([A (K), Y)) = if (A (K) < Y, Y - A (K), 0)$
201		iftrue	$⊢ A (K) < Y \to if (A (K) < Y, Y - A (K), 0) = Y - A (K)$
202	201	adantl	$⊢ (φ \land A (K) < Y) \to if (A (K) < Y, Y - A (K), 0) = Y - A (K)$
203	200 202	eqtrd	$⊢ (φ \land A (K) < Y) \to vol ([A (K), Y)) = Y - A (K)$
204	203	adantlr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to vol ([A (K), Y)) = Y - A (K)$
205	3	adantr	$⊢ (φ \land Y < B (K)) \to Y \in ℝ$
206	77	adantr	$⊢ (φ \land Y < B (K)) \to B (K) \in ℝ$
207		volico	$⊢ (Y \in ℝ \land B (K) \in ℝ) \to vol ([Y, B (K))) = if (Y < B (K), B (K) - Y, 0)$
208	205 206 207	syl2anc	$⊢ (φ \land Y < B (K)) \to vol ([Y, B (K))) = if (Y < B (K), B (K) - Y, 0)$
209		iftrue	$⊢ Y < B (K) \to if (Y < B (K), B (K) - Y, 0) = B (K) - Y$
210	209	adantl	$⊢ (φ \land Y < B (K)) \to if (Y < B (K), B (K) - Y, 0) = B (K) - Y$
211	208 210	eqtrd	$⊢ (φ \land Y < B (K)) \to vol ([Y, B (K))) = B (K) - Y$
212	211	adantr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to vol ([Y, B (K))) = B (K) - Y$
213	204 212	oveq12d	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to vol ([A (K), Y)) + vol ([Y, B (K))) = (Y - A (K)) + B (K) - Y$
214	190 196 213	syl2anc	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to vol ([A (K), Y)) + vol ([Y, B (K))) = (Y - A (K)) + B (K) - Y$
215	197	adantlr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to A (K) \in ℝ$
216	205	adantr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to Y \in ℝ$
217	206	adantr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to B (K) \in ℝ$
218		simpr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to A (K) < Y$
219		simplr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to Y < B (K)$
220	215 216 217 218 219	lttrd	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to A (K) < B (K)$
221	220	iftrued	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to if (A (K) < B (K), B (K) - A (K), 0) = B (K) - A (K)$
222	221	eqcomd	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to B (K) - A (K) = if (A (K) < B (K), B (K) - A (K), 0)$
223	3 49	resubcld	$⊢ φ \to Y - A (K) \in ℝ$
224	223	recnd	$⊢ φ \to Y - A (K) \in ℂ$
225	77 3	resubcld	$⊢ φ \to B (K) - Y \in ℝ$
226	225	recnd	$⊢ φ \to B (K) - Y \in ℂ$
227	224 226	addcomd	$⊢ φ \to (Y - A (K)) + B (K) - Y = (B (K) - Y) + Y - A (K)$
228	77	recnd	$⊢ φ \to B (K) \in ℂ$
229	3	recnd	$⊢ φ \to Y \in ℂ$
230	49	recnd	$⊢ φ \to A (K) \in ℂ$
231	228 229 230	npncand	$⊢ φ \to (B (K) - Y) + Y - A (K) = B (K) - A (K)$
232	227 231	eqtrd	$⊢ φ \to (Y - A (K)) + B (K) - Y = B (K) - A (K)$
233	232	ad2antrr	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to (Y - A (K)) + B (K) - Y = B (K) - A (K)$
234		volico	$⊢ (A (K) \in ℝ \land B (K) \in ℝ) \to vol ([A (K), B (K))) = if (A (K) < B (K), B (K) - A (K), 0)$
235	215 217 234	syl2anc	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to vol ([A (K), B (K))) = if (A (K) < B (K), B (K) - A (K), 0)$
236	222 233 235	3eqtr4d	$⊢ ((φ \land Y < B (K)) \land A (K) < Y) \to (Y - A (K)) + B (K) - Y = vol ([A (K), B (K)))$
237	190 196 236	syl2anc	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to (Y - A (K)) + B (K) - Y = vol ([A (K), B (K)))$
238	189 214 237	3eqtrd	$⊢ ((φ \land Y < B (K)) \land \neg Y \leq A (K)) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
239	186 238	pm2.61dan	$⊢ (φ \land Y < B (K)) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
240	163 168 239	syl2anc	$⊢ (φ \land \neg B (K) \leq Y) \to vol ([A (K), Y)) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
241	162 240	eqtrd	$⊢ (φ \land \neg B (K) \leq Y) \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
242	157 241	pm2.61dan	$⊢ φ \to vol ([A (K), if (B (K) \leq Y, B (K), Y))) + vol ([if (Y \leq A (K), A (K), Y), B (K))) = vol ([A (K), B (K)))$
243	115 242	eqtr2d	$⊢ φ \to vol ([A (K), B (K))) = vol ([A (K), T (Y) (B) (K))) + vol ([S (Y) (A) (K), B (K)))$
244	243	oveq2d	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), B (K))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) (vol ([A (K), T (Y) (B) (K))) + vol ([S (Y) (A) (K), B (K))))$
245	32 96	fprodcl	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) \in ℂ$
246	245 53 80	adddid	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) (vol ([A (K), T (Y) (B) (K))) + vol ([S (Y) (A) (K), B (K)))) = \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), T (Y) (B) (K))) + \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([S (Y) (A) (K), B (K)))$
247	103 244 246	3eqtrrd	$⊢ φ \to \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([A (K), T (Y) (B) (K))) + \prod_{k \in X ∖ \{K\}} vol ([A (k), B (k))) vol ([S (Y) (A) (K), B (K))) = \prod_{k \in X} vol ([A (k), B (k)))$
248	20 93 247	3eqtrd	$⊢ φ \to (A L (X) T (Y) (B)) + (S (Y) (A) L (X) B) = \prod_{k \in X} vol ([A (k), B (k)))$
249	6 1 17 4 5	hoidmvn0val	$⊢ φ \to A L (X) B = \prod_{k \in X} vol ([A (k), B (k)))$
250	249	eqcomd	$⊢ φ \to \prod_{k \in X} vol ([A (k), B (k))) = A L (X) B$
251	16 248 250	3eqtrrd	$⊢ φ \to A L (X) B = (A L (X) T (Y) (B)) +_{𝑒} (S (Y) (A) L (X) B)$

Metamath Proof Explorer

Theorem hspmbllem1

Proof