hspmbllem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > hspmbllem1		Structured version Visualization version GIF version

Theorem hspmbllem1 44857

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.)

**Hypotheses**
Ref	Expression
hspmbllem1.x	⊢ (𝜑 → 𝑋 ∈ Fin)
hspmbllem1.k	⊢ (𝜑 → 𝐾 ∈ 𝑋)
hspmbllem1.y	⊢ (𝜑 → 𝑌 ∈ ℝ)
hspmbllem1.a	⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
hspmbllem1.b	⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
hspmbllem1.l	⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hspmbllem1.t	⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
hspmbllem1.s	⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))

**Assertion**
Ref	Expression
hspmbllem1	⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Distinct variable groups: 𝐴,𝑎,𝑏,𝑘 𝐴,𝑐,ℎ,𝑘 𝐵,𝑎,𝑏,𝑘 𝐵,𝑐,ℎ 𝐾,𝑐,ℎ,𝑘,𝑥 𝑦,𝐾,𝑐,ℎ,𝑘 𝑆,𝑎,𝑏,𝑘 𝑇,𝑎,𝑏,𝑘 𝑋,𝑎,𝑏,𝑘,𝑥 𝑋,𝑐,ℎ,𝑦 𝑌,𝑎,𝑏,𝑘,𝑥 𝑌,𝑐,ℎ,𝑦 𝜑,𝑎,𝑏,𝑘,𝑥 𝜑,𝑐,ℎ,𝑦 Allowed substitution hints: 𝐴(𝑥,𝑦) 𝐵(𝑥,𝑦) 𝑆(𝑥,𝑦,ℎ,𝑐) 𝑇(𝑥,𝑦,ℎ,𝑐) 𝐾(𝑎,𝑏) 𝐿(𝑥,𝑦,ℎ,𝑘,𝑎,𝑏,𝑐)

**Proof of Theorem hspmbllem1**
Step	Hyp	Ref	Expression
1		rge0ssre 13373	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
2		hspmbllem1.l	. . . . 5 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_m 𝑥), 𝑏 ∈ (ℝ ↑_m 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
3		hspmbllem1.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		hspmbllem1.a	. . . . 5 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
5		hspmbllem1.t	. . . . . 6 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
6		hspmbllem1.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
7		hspmbllem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	5, 6, 3, 7	hsphoif 44807	. . . . 5 ⊢ (𝜑 → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
9	2, 3, 4, 8	hoidmvcl 44813	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ (0[,)+∞))
10	1, 9	sselid 3942	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ ℝ)
11		hspmbllem1.s	. . . . . 6 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
12	11, 6, 3, 4	hoidifhspf 44849	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
13	2, 3, 12, 7	hoidmvcl 44813	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ (0[,)+∞))
14	1, 13	sselid 3942	. . 3 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ ℝ)
15	10, 14	rexaddd 13153	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))
16		hspmbllem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
17	16	ne0d 4295	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ ∅)
18	2, 3, 17, 4, 8	hoidmvn0val 44815	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
19	2, 3, 17, 12, 7	hoidmvn0val 44815	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
20	18, 19	oveq12d 7375	. . 3 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))))
21		uncom 4113	. . . . . . . . 9 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
22	21	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
23	16	snssd 4769	. . . . . . . . 9 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
24		undif 4441	. . . . . . . . 9 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
25	23, 24	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
26	22, 25	eqtrd 2776	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
27	26	eqcomd 2742	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
28	27	prodeq1d 15804	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
29		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑘𝜑
30		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
31		difssd 4092	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
32	3, 31	ssfid 9211	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33		neldifsnd 4753	. . . . . 6 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
34	4	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
35	31	sselda 3944	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘 ∈ 𝑋)
36	34, 35	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴‘𝑘) ∈ ℝ)
37	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
38	3	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
39	7	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
40	5, 37, 38, 39	hsphoif 44807	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
41	40, 35	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42		volicore 44812	. . . . . . . 8 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
43	36, 41, 42	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
44	43	recnd 11183	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45		fveq2 6842	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
46		fveq2 6842	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (((𝑇‘𝑌)‘𝐵)‘𝐾))
47	45, 46	oveq12d 7375	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
48	47	fveq2d 6846	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))))
49	4, 16	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ)
50	8, 16	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51		volicore 44812	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
52	49, 50, 51	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
53	52	recnd 11183	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
54	29, 30, 32, 16, 33, 44, 48, 53	fprodsplitsn 15872	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
55	5, 37, 38, 39, 35	hsphoival 44810	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)))
56		iftrue 4492	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
57	56	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
58	55, 57	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (𝐵‘𝑘))
59	58	oveq2d 7373	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
60	59	fveq2d 6846	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
61	60	prodeq2dv 15806	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
62	61	oveq1d 7372	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
63	28, 54, 62	3eqtrd 2780	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
64	27	prodeq1d 15804	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
65		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
66	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
67	66, 35	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ)
68	58, 41	eqeltrrd 2839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵‘𝑘) ∈ ℝ)
69		volicore 44812	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
70	67, 68, 69	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
71	70	recnd 11183	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
72		fveq2 6842	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (((𝑆‘𝑌)‘𝐴)‘𝐾))
73		fveq2 6842	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐵‘𝑘) = (𝐵‘𝐾))
74	72, 73	oveq12d 7375	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
75	74	fveq2d 6846	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))
76	12, 16	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ)
77	7, 16	ffvelcdmd 7036	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ)
78		volicore 44812	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
79	76, 77, 78	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
80	79	recnd 11183	. . . . . 6 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
81	29, 65, 32, 16, 33, 71, 75, 80	fprodsplitsn 15872	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
82	11, 37, 38, 34, 35	hoidifhspval3 44850	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))
83		eldifsni 4750	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘 ≠ 𝐾)
84		neneq 2949	. . . . . . . . . . . 12 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾)
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
86	85	iffalsed 4497	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
87	86	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
88	82, 87	eqtrd 2776	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (𝐴‘𝑘))
89	88	fvoveq1d 7379	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
90	89	prodeq2dv 15806	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
91	90	oveq1d 7372	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
92	64, 81, 91	3eqtrd 2780	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
93	63, 92	oveq12d 7375	. . 3 ⊢ (𝜑 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
94	27	prodeq1d 15804	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
95		nfcv 2907	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))
96	60, 44	eqeltrrd 2839	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
97	45, 73	oveq12d 7375	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
98	97	fveq2d 6846	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
99		volicore 44812	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
100	49, 77, 99	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
101	100	recnd 11183	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
102	29, 95, 32, 16, 33, 96, 98, 101	fprodsplitsn 15872	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
103	94, 102	eqtrd 2776	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
104	5, 6, 3, 7, 16	hsphoival 44810	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
105	33	iffalsed 4497	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
106	104, 105	eqtrd 2776	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
107	106	oveq2d 7373	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)) = ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
108	107	fveq2d 6846	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))))
109	11, 6, 3, 4, 16	hoidifhspval3 44850	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)))
110		eqid 2736	. . . . . . . . . . 11 ⊢ 𝐾 = 𝐾
111	110	iftruei 4493	. . . . . . . . . 10 ⊢ if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)
112	111	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
113	109, 112	eqtrd 2776	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
114	113	fvoveq1d 7379	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) = (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))))
115	108, 114	oveq12d 7375	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
116		iftrue 4492	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = (𝐵‘𝐾))
117	116	oveq2d 7373	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
118	117	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
119	118	oveq1d 7372	. . . . . . . . 9 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
120	119	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
121		iftrue 4492	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = (𝐴‘𝐾))
122	121	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
123	122	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
124	77	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
125	6	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
126	49	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
127		simplr 767	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ 𝑌)
128		simpr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
129	124, 125, 126, 127, 128	letrd 11312	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ (𝐴‘𝐾))
130	126	rexrd 11205	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
131	124	rexrd 11205	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ^*)
132		ico0 13310	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
133	130, 131, 132	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
134	129, 133	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅)
135	123, 134	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
136		iffalse 4495	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = 𝑌)
137	136	oveq1d 7372	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
138	137	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
139		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ≤ 𝑌)
140	6	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
141	140	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ^*)
142	77	rexrd 11205	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ^*)
143	142	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ^*)
144		ico0 13310	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
145	141, 143, 144	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
146	139, 145	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝑌[,)(𝐵‘𝐾)) = ∅)
147	146	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝑌[,)(𝐵‘𝐾)) = ∅)
148	138, 147	eqtrd 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
149	135, 148	pm2.61dan 811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
150	149	fveq2d 6846	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘∅))
151		vol0 44190	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
152	151	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153	150, 152	eqtrd 2776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = 0)
154	153	oveq2d 7373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0))
155	101	addid1d 11355	. . . . . . . . 9 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
156	155	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
157	120, 154, 156	3eqtrd 2780	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
158		iffalse 4495	. . . . . . . . . . . 12 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = 𝑌)
159	158	oveq2d 7373	. . . . . . . . . . 11 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)𝑌))
160	159	fveq2d 6846	. . . . . . . . . 10 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
161	160	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
162	161	oveq1d 7372	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
163		simpl 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝜑)
164		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ¬ (𝐵‘𝐾) ≤ 𝑌)
165	163, 6	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
166	163, 77	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ)
167	165, 166	ltnled 11302	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝑌 < (𝐵‘𝐾) ↔ ¬ (𝐵‘𝐾) ≤ 𝑌))
168	164, 167	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 < (𝐵‘𝐾))
169	121	fvoveq1d 7379	. . . . . . . . . . . . 13 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
170	169	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
171	170	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
172		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
173	49	rexrd 11205	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ^*)
174	173	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
175	140	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ^*)
176		ico0 13310	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ 𝑌 ∈ ℝ^*) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
177	174, 175, 176	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
178	172, 177	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)𝑌) = ∅)
179	178	fveq2d 6846	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (vol‘∅))
180	151	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘∅) = 0)
181	179, 180	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = 0)
182	181	oveq1d 7372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
183	182	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
184	101	addid2d 11356	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
185	184	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
186	171, 183, 185	3eqtrd 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
187	136	fvoveq1d 7379	. . . . . . . . . . . . 13 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘(𝑌[,)(𝐵‘𝐾))))
188	187	oveq2d 7373	. . . . . . . . . . . 12 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
189	188	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
190		simpl 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝜑 ∧ 𝑌 < (𝐵‘𝐾)))
191		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ¬ 𝑌 ≤ (𝐴‘𝐾))
192	49	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
193	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
194	192, 193	ltnled 11302	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴‘𝐾)))
195	191, 194	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
196	195	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
197	49	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
198	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199		volico 44214	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
200	197, 198, 199	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
201		iftrue 4492	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝐾) < 𝑌 → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
202	201	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
203	200, 202	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
204	203	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
205	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → 𝑌 ∈ ℝ)
206	77	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
207		volico 44214	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
208	205, 206, 207	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
209		iftrue 4492	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 < (𝐵‘𝐾) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
210	209	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
211	208, 210	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
212	211	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
213	204, 212	oveq12d 7375	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
214	190, 196, 213	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
215	197	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
216	205	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
217	206	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐵‘𝐾) ∈ ℝ)
218		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < 𝑌)
219		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 < (𝐵‘𝐾))
220	215, 216, 217, 218, 219	lttrd 11316	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < (𝐵‘𝐾))
221	220	iftrued 4494	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
222	221	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝐵‘𝐾) − (𝐴‘𝐾)) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
223	6, 49	resubcld 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℝ)
224	223	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℂ)
225	77, 6	resubcld 11583	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℝ)
226	225	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℂ)
227	224, 226	addcomd 11357	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))))
228	77	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℂ)
229	6	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
230	49	recnd 11183	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
231	228, 229, 230	npncand 11536	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
232	227, 231	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
233	232	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
234		volico 44214	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
235	215, 217, 234	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
236	222, 233, 235	3eqtr4d 2786	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
237	190, 196, 236	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
238	189, 214, 237	3eqtrd 2780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
239	186, 238	pm2.61dan 811	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
240	163, 168, 239	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
241	162, 240	eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
242	157, 241	pm2.61dan 811	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
243	115, 242	eqtr2d 2777	. . . . 5 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
244	243	oveq2d 7373	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
245	32, 96	fprodcl 15835	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
246	245, 53, 80	adddid 11179	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
247	103, 244, 246	3eqtrrd 2781	. . 3 ⊢ (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
248	20, 93, 247	3eqtrd 2780	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
249	2, 3, 17, 4, 7	hoidmvn0val 44815	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
250	249	eqcomd 2742	. 2 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵))
251	15, 248, 250	3eqtrrd 2781	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∖ cdif 3907 ∪ cun 3908 ⊆ wss 3910 ∅c0 4282 ifcif 4486 {csn 4586 class class class wbr 5105 ↦ cmpt 5188 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ∈ cmpo 7359 ↑_m cmap 8765 Fincfn 8883 ℂcc 11049 ℝcr 11050 0cc0 11051 + caddc 11054 · cmul 11056 +∞cpnf 11186 ℝ^*cxr 11188 < clt 11189 ≤ cle 11190 − cmin 11385 +_𝑒 cxad 13031 [,)cico 13266 ∏cprod 15788 volcvol 24827

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672 ax-inf2 9577 ax-cnex 11107 ax-resscn 11108 ax-1cn 11109 ax-icn 11110 ax-addcl 11111 ax-addrcl 11112 ax-mulcl 11113 ax-mulrcl 11114 ax-mulcom 11115 ax-addass 11116 ax-mulass 11117 ax-distr 11118 ax-i2m1 11119 ax-1ne0 11120 ax-1rid 11121 ax-rnegex 11122 ax-rrecex 11123 ax-cnre 11124 ax-pre-lttri 11125 ax-pre-lttrn 11126 ax-pre-ltadd 11127 ax-pre-mulgt0 11128 ax-pre-sup 11129

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3065 df-rex 3074 df-rmo 3353 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-se 5589 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-isom 6505 df-riota 7313 df-ov 7360 df-oprab 7361 df-mpo 7362 df-of 7617 df-om 7803 df-1st 7921 df-2nd 7922 df-frecs 8212 df-wrecs 8243 df-recs 8317 df-rdg 8356 df-1o 8412 df-2o 8413 df-er 8648 df-map 8767 df-pm 8768 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9347 df-sup 9378 df-inf 9379 df-oi 9446 df-dju 9837 df-card 9875 df-pnf 11191 df-mnf 11192 df-xr 11193 df-ltxr 11194 df-le 11195 df-sub 11387 df-neg 11388 df-div 11813 df-nn 12154 df-2 12216 df-3 12217 df-n0 12414 df-z 12500 df-uz 12764 df-q 12874 df-rp 12916 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13268 df-ico 13270 df-icc 13271 df-fz 13425 df-fzo 13568 df-fl 13697 df-seq 13907 df-exp 13968 df-hash 14231 df-cj 14984 df-re 14985 df-im 14986 df-sqrt 15120 df-abs 15121 df-clim 15370 df-rlim 15371 df-sum 15571 df-prod 15789 df-rest 17304 df-topgen 17325 df-psmet 20788 df-xmet 20789 df-met 20790 df-bl 20791 df-mopn 20792 df-top 22243 df-topon 22260 df-bases 22296 df-cmp 22738 df-ovol 24828 df-vol 24829

This theorem is referenced by: hspmbllem2 44858

W3C validator