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 45332

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 13432	. . . 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 45282	. . . . 5 ⊢ (𝜑 → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
9	2, 3, 4, 8	hoidmvcl 45288	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ (0[,)+∞))
10	1, 9	sselid 3980	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ ℝ)
11		hspmbllem1.s	. . . . . 6 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
12	11, 6, 3, 4	hoidifhspf 45324	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
13	2, 3, 12, 7	hoidmvcl 45288	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ (0[,)+∞))
14	1, 13	sselid 3980	. . 3 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ ℝ)
15	10, 14	rexaddd 13212	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))
16		hspmbllem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
17	16	ne0d 4335	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ ∅)
18	2, 3, 17, 4, 8	hoidmvn0val 45290	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
19	2, 3, 17, 12, 7	hoidmvn0val 45290	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
20	18, 19	oveq12d 7426	. . 3 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))))
21		uncom 4153	. . . . . . . . 9 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
22	21	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
23	16	snssd 4812	. . . . . . . . 9 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
24		undif 4481	. . . . . . . . 9 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
25	23, 24	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
26	22, 25	eqtrd 2772	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
27	26	eqcomd 2738	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
28	27	prodeq1d 15864	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
29		nfv 1917	. . . . . 6 ⊢ Ⅎ𝑘𝜑
30		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
31		difssd 4132	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
32	3, 31	ssfid 9266	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33		neldifsnd 4796	. . . . . 6 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
34	4	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
35	31	sselda 3982	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘 ∈ 𝑋)
36	34, 35	ffvelcdmd 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴‘𝑘) ∈ ℝ)
37	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
38	3	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
39	7	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
40	5, 37, 38, 39	hsphoif 45282	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
41	40, 35	ffvelcdmd 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42		volicore 45287	. . . . . . . 8 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
43	36, 41, 42	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
44	43	recnd 11241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45		fveq2 6891	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
46		fveq2 6891	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (((𝑇‘𝑌)‘𝐵)‘𝐾))
47	45, 46	oveq12d 7426	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
48	47	fveq2d 6895	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))))
49	4, 16	ffvelcdmd 7087	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ)
50	8, 16	ffvelcdmd 7087	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51		volicore 45287	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
52	49, 50, 51	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
53	52	recnd 11241	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
54	29, 30, 32, 16, 33, 44, 48, 53	fprodsplitsn 15932	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
55	5, 37, 38, 39, 35	hsphoival 45285	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)))
56		iftrue 4534	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
57	56	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
58	55, 57	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (𝐵‘𝑘))
59	58	oveq2d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
60	59	fveq2d 6895	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
61	60	prodeq2dv 15866	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
62	61	oveq1d 7423	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
63	28, 54, 62	3eqtrd 2776	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
64	27	prodeq1d 15864	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
65		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
66	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
67	66, 35	ffvelcdmd 7087	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ)
68	58, 41	eqeltrrd 2834	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵‘𝑘) ∈ ℝ)
69		volicore 45287	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
70	67, 68, 69	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
71	70	recnd 11241	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
72		fveq2 6891	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (((𝑆‘𝑌)‘𝐴)‘𝐾))
73		fveq2 6891	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐵‘𝑘) = (𝐵‘𝐾))
74	72, 73	oveq12d 7426	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
75	74	fveq2d 6895	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))
76	12, 16	ffvelcdmd 7087	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ)
77	7, 16	ffvelcdmd 7087	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ)
78		volicore 45287	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
79	76, 77, 78	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
80	79	recnd 11241	. . . . . 6 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
81	29, 65, 32, 16, 33, 71, 75, 80	fprodsplitsn 15932	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
82	11, 37, 38, 34, 35	hoidifhspval3 45325	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))
83		eldifsni 4793	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘 ≠ 𝐾)
84		neneq 2946	. . . . . . . . . . . 12 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾)
85	83, 84	syl 17	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
86	85	iffalsed 4539	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
87	86	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
88	82, 87	eqtrd 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (𝐴‘𝑘))
89	88	fvoveq1d 7430	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
90	89	prodeq2dv 15866	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
91	90	oveq1d 7423	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
92	64, 81, 91	3eqtrd 2776	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
93	63, 92	oveq12d 7426	. . 3 ⊢ (𝜑 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
94	27	prodeq1d 15864	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
95		nfcv 2903	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))
96	60, 44	eqeltrrd 2834	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
97	45, 73	oveq12d 7426	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
98	97	fveq2d 6895	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
99		volicore 45287	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
100	49, 77, 99	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
101	100	recnd 11241	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
102	29, 95, 32, 16, 33, 96, 98, 101	fprodsplitsn 15932	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
103	94, 102	eqtrd 2772	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
104	5, 6, 3, 7, 16	hsphoival 45285	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
105	33	iffalsed 4539	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
106	104, 105	eqtrd 2772	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
107	106	oveq2d 7424	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)) = ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
108	107	fveq2d 6895	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))))
109	11, 6, 3, 4, 16	hoidifhspval3 45325	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)))
110		eqid 2732	. . . . . . . . . . 11 ⊢ 𝐾 = 𝐾
111	110	iftruei 4535	. . . . . . . . . 10 ⊢ if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)
112	111	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
113	109, 112	eqtrd 2772	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
114	113	fvoveq1d 7430	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) = (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))))
115	108, 114	oveq12d 7426	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
116		iftrue 4534	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = (𝐵‘𝐾))
117	116	oveq2d 7424	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
118	117	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
119	118	oveq1d 7423	. . . . . . . . 9 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
120	119	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
121		iftrue 4534	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = (𝐴‘𝐾))
122	121	oveq1d 7423	. . . . . . . . . . . . . 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 11370	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ (𝐴‘𝐾))
130	126	rexrd 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
131	124	rexrd 11263	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ^*)
132		ico0 13369	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
133	130, 131, 132	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
134	129, 133	mpbird 256	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅)
135	123, 134	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
136		iffalse 4537	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = 𝑌)
137	136	oveq1d 7423	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
138	137	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
139		simpr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ≤ 𝑌)
140	6	rexrd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
141	140	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ^*)
142	77	rexrd 11263	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ^*)
143	142	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ^*)
144		ico0 13369	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
145	141, 143, 144	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
146	139, 145	mpbird 256	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝑌[,)(𝐵‘𝐾)) = ∅)
147	146	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝑌[,)(𝐵‘𝐾)) = ∅)
148	138, 147	eqtrd 2772	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
149	135, 148	pm2.61dan 811	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
150	149	fveq2d 6895	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘∅))
151		vol0 44665	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
152	151	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153	150, 152	eqtrd 2772	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = 0)
154	153	oveq2d 7424	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0))
155	101	addridd 11413	. . . . . . . . 9 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
156	155	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
157	120, 154, 156	3eqtrd 2776	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
158		iffalse 4537	. . . . . . . . . . . 12 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = 𝑌)
159	158	oveq2d 7424	. . . . . . . . . . 11 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)𝑌))
160	159	fveq2d 6895	. . . . . . . . . 10 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
161	160	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
162	161	oveq1d 7423	. . . . . . . 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 11360	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝑌 < (𝐵‘𝐾) ↔ ¬ (𝐵‘𝐾) ≤ 𝑌))
168	164, 167	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 < (𝐵‘𝐾))
169	121	fvoveq1d 7430	. . . . . . . . . . . . 13 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
170	169	oveq2d 7424	. . . . . . . . . . . 12 ⊢ (𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
171	170	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
172		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
173	49	rexrd 11263	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ^*)
174	173	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
175	140	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ^*)
176		ico0 13369	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ 𝑌 ∈ ℝ^*) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
177	174, 175, 176	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
178	172, 177	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)𝑌) = ∅)
179	178	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (vol‘∅))
180	151	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘∅) = 0)
181	179, 180	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = 0)
182	181	oveq1d 7423	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
183	182	adantlr 713	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
184	101	addlidd 11414	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
185	184	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
186	171, 183, 185	3eqtrd 2776	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
187	136	fvoveq1d 7430	. . . . . . . . . . . . 13 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘(𝑌[,)(𝐵‘𝐾))))
188	187	oveq2d 7424	. . . . . . . . . . . 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 11360	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴‘𝐾)))
195	191, 194	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
196	195	adantlr 713	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
197	49	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
198	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199		volico 44689	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
200	197, 198, 199	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
201		iftrue 4534	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝐾) < 𝑌 → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
202	201	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
203	200, 202	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
204	203	adantlr 713	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
205	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → 𝑌 ∈ ℝ)
206	77	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
207		volico 44689	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
208	205, 206, 207	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
209		iftrue 4534	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 < (𝐵‘𝐾) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
210	209	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
211	208, 210	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
212	211	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
213	204, 212	oveq12d 7426	. . . . . . . . . . . 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 11374	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < (𝐵‘𝐾))
221	220	iftrued 4536	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
222	221	eqcomd 2738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝐵‘𝐾) − (𝐴‘𝐾)) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
223	6, 49	resubcld 11641	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℝ)
224	223	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℂ)
225	77, 6	resubcld 11641	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℝ)
226	225	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℂ)
227	224, 226	addcomd 11415	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))))
228	77	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℂ)
229	6	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
230	49	recnd 11241	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
231	228, 229, 230	npncand 11594	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
232	227, 231	eqtrd 2772	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
233	232	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
234		volico 44689	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
235	215, 217, 234	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
236	222, 233, 235	3eqtr4d 2782	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
237	190, 196, 236	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
238	189, 214, 237	3eqtrd 2776	. . . . . . . . . 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 2772	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
242	157, 241	pm2.61dan 811	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
243	115, 242	eqtr2d 2773	. . . . 5 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
244	243	oveq2d 7424	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
245	32, 96	fprodcl 15895	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
246	245, 53, 80	adddid 11237	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
247	103, 244, 246	3eqtrrd 2777	. . 3 ⊢ (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
248	20, 93, 247	3eqtrd 2776	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
249	2, 3, 17, 4, 7	hoidmvn0val 45290	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
250	249	eqcomd 2738	. 2 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵))
251	15, 248, 250	3eqtrrd 2777	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∖ cdif 3945 ∪ cun 3946 ⊆ wss 3948 ∅c0 4322 ifcif 4528 {csn 4628 class class class wbr 5148 ↦ cmpt 5231 ⟶wf 6539 ‘cfv 6543 (class class class)co 7408 ∈ cmpo 7410 ↑_m cmap 8819 Fincfn 8938 ℂcc 11107 ℝcr 11108 0cc0 11109 + caddc 11112 · cmul 11114 +∞cpnf 11244 ℝ^*cxr 11246 < clt 11247 ≤ cle 11248 − cmin 11443 +_𝑒 cxad 13089 [,)cico 13325 ∏cprod 15848 volcvol 24979

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 2703 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7724 ax-inf2 9635 ax-cnex 11165 ax-resscn 11166 ax-1cn 11167 ax-icn 11168 ax-addcl 11169 ax-addrcl 11170 ax-mulcl 11171 ax-mulrcl 11172 ax-mulcom 11173 ax-addass 11174 ax-mulass 11175 ax-distr 11176 ax-i2m1 11177 ax-1ne0 11178 ax-1rid 11179 ax-rnegex 11180 ax-rrecex 11181 ax-cnre 11182 ax-pre-lttri 11183 ax-pre-lttrn 11184 ax-pre-ltadd 11185 ax-pre-mulgt0 11186 ax-pre-sup 11187

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 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7364 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7669 df-om 7855 df-1st 7974 df-2nd 7975 df-frecs 8265 df-wrecs 8296 df-recs 8370 df-rdg 8409 df-1o 8465 df-2o 8466 df-er 8702 df-map 8821 df-pm 8822 df-en 8939 df-dom 8940 df-sdom 8941 df-fin 8942 df-fi 9405 df-sup 9436 df-inf 9437 df-oi 9504 df-dju 9895 df-card 9933 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11445 df-neg 11446 df-div 11871 df-nn 12212 df-2 12274 df-3 12275 df-n0 12472 df-z 12558 df-uz 12822 df-q 12932 df-rp 12974 df-xneg 13091 df-xadd 13092 df-xmul 13093 df-ioo 13327 df-ico 13329 df-icc 13330 df-fz 13484 df-fzo 13627 df-fl 13756 df-seq 13966 df-exp 14027 df-hash 14290 df-cj 15045 df-re 15046 df-im 15047 df-sqrt 15181 df-abs 15182 df-clim 15431 df-rlim 15432 df-sum 15632 df-prod 15849 df-rest 17367 df-topgen 17388 df-psmet 20935 df-xmet 20936 df-met 20937 df-bl 20938 df-mopn 20939 df-top 22395 df-topon 22412 df-bases 22448 df-cmp 22890 df-ovol 24980 df-vol 24981

This theorem is referenced by: hspmbllem2 45333

W3C validator