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 47373

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 13494	. . . 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 47323	. . . . 5 ⊢ (𝜑 → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
9	2, 3, 4, 8	hoidmvcl 47329	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ (0[,)+∞))
10	1, 9	sselid 3936	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ ℝ)
11		hspmbllem1.s	. . . . . 6 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
12	11, 6, 3, 4	hoidifhspf 47365	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
13	2, 3, 12, 7	hoidmvcl 47329	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ (0[,)+∞))
14	1, 13	sselid 3936	. . 3 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ ℝ)
15	10, 14	rexaddd 13271	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))
16		hspmbllem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
17	16	ne0d 4295	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ ∅)
18	2, 3, 17, 4, 8	hoidmvn0val 47331	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
19	2, 3, 17, 12, 7	hoidmvn0val 47331	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
20	18, 19	oveq12d 7434	. . 3 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))))
21		uncom 4112	. . . . . . . . 9 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
22	21	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
23	16	snssd 4754	. . . . . . . . 9 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
24		undif 4445	. . . . . . . . 9 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
25	23, 24	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
26	22, 25	eqtrd 2800	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
27	26	eqcomd 2771	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
28	27	prodeq1d 15992	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
29		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑘𝜑
30		nfcv 2927	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
31		difssd 4091	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
32	3, 31	ssfid 9232	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33		neldifsnd 4763	. . . . . 6 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
34	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
35	31	sselda 3938	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘 ∈ 𝑋)
36	34, 35	ffvelcdmd 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴‘𝑘) ∈ ℝ)
37	6	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
38	3	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
39	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
40	5, 37, 38, 39	hsphoif 47323	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
41	40, 35	ffvelcdmd 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42		volicore 47328	. . . . . . . 8 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
43	36, 41, 42	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
44	43	recnd 11248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45		fveq2 6885	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
46		fveq2 6885	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (((𝑇‘𝑌)‘𝐵)‘𝐾))
47	45, 46	oveq12d 7434	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
48	47	fveq2d 6889	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))))
49	4, 16	ffvelcdmd 7084	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ)
50	8, 16	ffvelcdmd 7084	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51		volicore 47328	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
52	49, 50, 51	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
53	52	recnd 11248	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
54	29, 30, 32, 16, 33, 44, 48, 53	fprodsplitsn 16061	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
55	5, 37, 38, 39, 35	hsphoival 47326	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)))
56		iftrue 4495	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
57	56	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
58	55, 57	eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (𝐵‘𝑘))
59	58	oveq2d 7432	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
60	59	fveq2d 6889	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
61	60	prodeq2dv 15994	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
62	61	oveq1d 7431	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
63	28, 54, 62	3eqtrd 2804	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
64	27	prodeq1d 15992	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
65		nfcv 2927	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
66	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
67	66, 35	ffvelcdmd 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ)
68	58, 41	eqeltrrd 2866	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵‘𝑘) ∈ ℝ)
69		volicore 47328	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
70	67, 68, 69	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
71	70	recnd 11248	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
72		fveq2 6885	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (((𝑆‘𝑌)‘𝐴)‘𝐾))
73		fveq2 6885	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐵‘𝑘) = (𝐵‘𝐾))
74	72, 73	oveq12d 7434	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
75	74	fveq2d 6889	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))
76	12, 16	ffvelcdmd 7084	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ)
77	7, 16	ffvelcdmd 7084	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ)
78		volicore 47328	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
79	76, 77, 78	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
80	79	recnd 11248	. . . . . 6 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
81	29, 65, 32, 16, 33, 71, 75, 80	fprodsplitsn 16061	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
82	11, 37, 38, 34, 35	hoidifhspval3 47366	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))
83		eldifsni 4760	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘 ≠ 𝐾)
84		neneq 2966	. . . . . . . . . . . 12 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾)
85	83, 84	syl 18	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
86	85	iffalsed 4500	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
87	86	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
88	82, 87	eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (𝐴‘𝑘))
89	88	fvoveq1d 7438	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
90	89	prodeq2dv 15994	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
91	90	oveq1d 7431	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
92	64, 81, 91	3eqtrd 2804	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
93	63, 92	oveq12d 7434	. . 3 ⊢ (𝜑 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
94	27	prodeq1d 15992	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
95		nfcv 2927	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))
96	60, 44	eqeltrrd 2866	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
97	45, 73	oveq12d 7434	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
98	97	fveq2d 6889	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
99		volicore 47328	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
100	49, 77, 99	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
101	100	recnd 11248	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
102	29, 95, 32, 16, 33, 96, 98, 101	fprodsplitsn 16061	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
103	94, 102	eqtrd 2800	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
104	5, 6, 3, 7, 16	hsphoival 47326	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
105	33	iffalsed 4500	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
106	104, 105	eqtrd 2800	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
107	106	oveq2d 7432	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)) = ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
108	107	fveq2d 6889	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))))
109	11, 6, 3, 4, 16	hoidifhspval3 47366	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)))
110		eqid 2765	. . . . . . . . . . 11 ⊢ 𝐾 = 𝐾
111	110	iftruei 4496	. . . . . . . . . 10 ⊢ if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)
112	111	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
113	109, 112	eqtrd 2800	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
114	113	fvoveq1d 7438	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) = (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))))
115	108, 114	oveq12d 7434	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
116		iftrue 4495	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = (𝐵‘𝐾))
117	116	oveq2d 7432	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
118	117	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
119	118	oveq1d 7431	. . . . . . . . 9 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
120	119	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
121		iftrue 4495	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = (𝐴‘𝐾))
122	121	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
123	122	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
124	77	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
125	6	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
126	49	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
127		simplr 781	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ 𝑌)
128		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
129	124, 125, 126, 127, 128	letrd 11378	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ (𝐴‘𝐾))
130	126	rexrd 11270	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
131	124	rexrd 11270	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ^*)
132		ico0 13429	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
133	130, 131, 132	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
134	129, 133	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅)
135	123, 134	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
136		iffalse 4498	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = 𝑌)
137	136	oveq1d 7431	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
138	137	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
139		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ≤ 𝑌)
140	6	rexrd 11270	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
141	140	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ^*)
142	77	rexrd 11270	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ^*)
143	142	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ^*)
144		ico0 13429	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
145	141, 143, 144	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
146	139, 145	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝑌[,)(𝐵‘𝐾)) = ∅)
147	146	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝑌[,)(𝐵‘𝐾)) = ∅)
148	138, 147	eqtrd 2800	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
149	135, 148	pm2.61dan 825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
150	149	fveq2d 6889	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘∅))
151		vol0 46706	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
152	151	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153	150, 152	eqtrd 2800	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = 0)
154	153	oveq2d 7432	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0))
155	101	addridd 11421	. . . . . . . . 9 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
156	155	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
157	120, 154, 156	3eqtrd 2804	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
158		iffalse 4498	. . . . . . . . . . . 12 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = 𝑌)
159	158	oveq2d 7432	. . . . . . . . . . 11 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)𝑌))
160	159	fveq2d 6889	. . . . . . . . . 10 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
161	160	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
162	161	oveq1d 7431	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
163		simpl 488	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝜑)
164		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ¬ (𝐵‘𝐾) ≤ 𝑌)
165	163, 6	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
166	163, 77	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ)
167	165, 166	ltnled 11368	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝑌 < (𝐵‘𝐾) ↔ ¬ (𝐵‘𝐾) ≤ 𝑌))
168	164, 167	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 < (𝐵‘𝐾))
169	121	fvoveq1d 7438	. . . . . . . . . . . . 13 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
170	169	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
171	170	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
172		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
173	49	rexrd 11270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ^*)
174	173	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
175	140	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ^*)
176		ico0 13429	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ 𝑌 ∈ ℝ^*) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
177	174, 175, 176	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
178	172, 177	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)𝑌) = ∅)
179	178	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (vol‘∅))
180	151	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘∅) = 0)
181	179, 180	eqtrd 2800	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = 0)
182	181	oveq1d 7431	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
183	182	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
184	101	addlidd 11422	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
185	184	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
186	171, 183, 185	3eqtrd 2804	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
187	136	fvoveq1d 7438	. . . . . . . . . . . . 13 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘(𝑌[,)(𝐵‘𝐾))))
188	187	oveq2d 7432	. . . . . . . . . . . 12 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
189	188	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
190		simpl 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝜑 ∧ 𝑌 < (𝐵‘𝐾)))
191		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ¬ 𝑌 ≤ (𝐴‘𝐾))
192	49	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
193	6	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
194	192, 193	ltnled 11368	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴‘𝐾)))
195	191, 194	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
196	195	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
197	49	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
198	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199		volico 46730	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
200	197, 198, 199	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
201		iftrue 4495	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝐾) < 𝑌 → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
202	201	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
203	200, 202	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
204	203	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
205	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → 𝑌 ∈ ℝ)
206	77	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
207		volico 46730	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
208	205, 206, 207	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
209		iftrue 4495	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 < (𝐵‘𝐾) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
210	209	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
211	208, 210	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
212	211	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
213	204, 212	oveq12d 7434	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
214	190, 196, 213	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
215	197	adantlr 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
216	205	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
217	206	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐵‘𝐾) ∈ ℝ)
218		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < 𝑌)
219		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 < (𝐵‘𝐾))
220	215, 216, 217, 218, 219	lttrd 11382	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < (𝐵‘𝐾))
221	220	iftrued 4497	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
222	221	eqcomd 2771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝐵‘𝐾) − (𝐴‘𝐾)) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
223	6, 49	resubcld 11653	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℝ)
224	223	recnd 11248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℂ)
225	77, 6	resubcld 11653	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℝ)
226	225	recnd 11248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℂ)
227	224, 226	addcomd 11423	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))))
228	77	recnd 11248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℂ)
229	6	recnd 11248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
230	49	recnd 11248	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
231	228, 229, 230	npncand 11604	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
232	227, 231	eqtrd 2800	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
233	232	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
234		volico 46730	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
235	215, 217, 234	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
236	222, 233, 235	3eqtr4d 2810	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
237	190, 196, 236	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
238	189, 214, 237	3eqtrd 2804	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
239	186, 238	pm2.61dan 825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
240	163, 168, 239	syl2anc 596	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
241	162, 240	eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
242	157, 241	pm2.61dan 825	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
243	115, 242	eqtr2d 2801	. . . . 5 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
244	243	oveq2d 7432	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
245	32, 96	fprodcl 16024	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
246	245, 53, 80	adddid 11244	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
247	103, 244, 246	3eqtrrd 2805	. . 3 ⊢ (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
248	20, 93, 247	3eqtrd 2804	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
249	2, 3, 17, 4, 7	hoidmvn0val 47331	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
250	249	eqcomd 2771	. 2 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵))
251	15, 248, 250	3eqtrrd 2805	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∖ cdif 3903 ∪ cun 3904 ⊆ wss 3906 ∅c0 4286 ifcif 4489 {csn 4591 class class class wbr 5111 ↦ cmpt 5194 ⟶wf 6536 ‘cfv 6540 (class class class)co 7416 ∈ cmpo 7418 ↑_m cmap 8826 Fincfn 8945 ℂcc 11109 ℝcr 11110 0cc0 11111 + caddc 11114 · cmul 11116 +∞cpnf 11251 ℝ^*cxr 11253 < clt 11254 ≤ cle 11255 − cmin 11452 +_𝑒 cxad 13146 [,)cico 13385 ∏cprod 15975 volcvol 25651

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7738 ax-inf2 9613 ax-cnex 11167 ax-resscn 11168 ax-1cn 11169 ax-icn 11170 ax-addcl 11171 ax-addrcl 11172 ax-mulcl 11173 ax-mulrcl 11174 ax-mulcom 11175 ax-addass 11176 ax-mulass 11177 ax-distr 11178 ax-i2m1 11179 ax-1ne0 11180 ax-1rid 11181 ax-rnegex 11182 ax-rrecex 11183 ax-cnre 11184 ax-pre-lttri 11185 ax-pre-lttrn 11186 ax-pre-ltadd 11187 ax-pre-mulgt0 11188 ax-pre-sup 11189

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7373 df-ov 7419 df-oprab 7420 df-mpo 7421 df-of 7680 df-om 7865 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8360 df-rdg 8399 df-1o 8455 df-2o 8456 df-er 8696 df-map 8828 df-pm 8829 df-en 8946 df-dom 8947 df-sdom 8948 df-fin 8949 df-fi 9374 df-sup 9405 df-inf 9406 df-oi 9475 df-dju 9899 df-card 9937 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11454 df-neg 11455 df-div 11883 df-nn 12245 df-2 12314 df-3 12315 df-n0 12516 df-z 12603 df-uz 12874 df-q 12984 df-rp 13028 df-xneg 13148 df-xadd 13149 df-xmul 13150 df-ioo 13387 df-ico 13389 df-icc 13390 df-fz 13547 df-fzo 13695 df-fl 13838 df-seq 14051 df-exp 14111 df-hash 14380 df-cj 15169 df-re 15170 df-im 15171 df-sqrt 15305 df-abs 15306 df-clim 15558 df-rlim 15559 df-sum 15757 df-prod 15976 df-rest 17492 df-topgen 17513 df-psmet 21543 df-xmet 21544 df-met 21545 df-bl 21546 df-mopn 21547 df-top 23080 df-topon 23097 df-bases 23132 df-cmp 23573 df-ovol 25652 df-vol 25653

This theorem is used by: hspmbllem2 47374

W3C validator