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 40840

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 ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
hspmbllem1.t	⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
hspmbllem1.s	⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))

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

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

**Proof of Theorem hspmbllem1**
Step	Hyp	Ref	Expression
1		rge0ssre 12280	. . . 4 ⊢ (0[,)+∞) ⊆ ℝ
2		hspmbllem1.l	. . . . 5 ⊢ 𝐿 = (𝑥 ∈ Fin ↦ (𝑎 ∈ (ℝ ↑_𝑚 𝑥), 𝑏 ∈ (ℝ ↑_𝑚 𝑥) ↦ if(𝑥 = ∅, 0, ∏𝑘 ∈ 𝑥 (vol‘((𝑎‘𝑘)[,)(𝑏‘𝑘))))))
3		hspmbllem1.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ Fin)
4		hspmbllem1.a	. . . . 5 ⊢ (𝜑 → 𝐴:𝑋⟶ℝ)
5		hspmbllem1.t	. . . . . 6 ⊢ 𝑇 = (𝑦 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ ∈ (𝑋 ∖ {𝐾}), (𝑐‘ℎ), if((𝑐‘ℎ) ≤ 𝑦, (𝑐‘ℎ), 𝑦)))))
6		hspmbllem1.y	. . . . . 6 ⊢ (𝜑 → 𝑌 ∈ ℝ)
7		hspmbllem1.b	. . . . . 6 ⊢ (𝜑 → 𝐵:𝑋⟶ℝ)
8	5, 6, 3, 7	hsphoif 40790	. . . . 5 ⊢ (𝜑 → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
9	2, 3, 4, 8	hoidmvcl 40796	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ (0[,)+∞))
10	1, 9	sseldi 3601	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ ℝ)
11		hspmbllem1.s	. . . . . 6 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_𝑚 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
12	11, 6, 3, 4	hoidifhspf 40832	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
13	2, 3, 12, 7	hoidmvcl 40796	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ (0[,)+∞))
14	1, 13	sseldi 3601	. . 3 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ ℝ)
15	10, 14	rexaddd 12065	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))
16		hspmbllem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
17		ne0i 3921	. . . . . 6 ⊢ (𝐾 ∈ 𝑋 → 𝑋 ≠ ∅)
18	16, 17	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ ∅)
19	2, 3, 18, 4, 8	hoidmvn0val 40798	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
20	2, 3, 18, 12, 7	hoidmvn0val 40798	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
21	19, 20	oveq12d 6668	. . 3 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))))
22		uncom 3757	. . . . . . . . 9 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
23	22	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
24	16	snssd 4340	. . . . . . . . 9 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
25		undif 4049	. . . . . . . . 9 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
26	24, 25	sylib 208	. . . . . . . 8 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
27	23, 26	eqtrd 2656	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
28	27	eqcomd 2628	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
29	28	prodeq1d 14651	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
30		nfv 1843	. . . . . 6 ⊢ Ⅎ𝑘𝜑
31		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
32		difssd 3738	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
33	3, 32	ssfid 8183	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
34		neldifsnd 4322	. . . . . 6 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
35	4	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
36	32	sselda 3603	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘 ∈ 𝑋)
37	35, 36	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴‘𝑘) ∈ ℝ)
38	6	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
39	3	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
40	7	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
41	5, 38, 39, 40	hsphoif 40790	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
42	41, 36	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ)
43		volicore 40795	. . . . . . . 8 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
44	37, 42, 43	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
45	44	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
46		fveq2 6191	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
47		fveq2 6191	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (((𝑇‘𝑌)‘𝐵)‘𝐾))
48	46, 47	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
49	48	fveq2d 6195	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))))
50	4, 16	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ)
51	8, 16	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ)
52		volicore 40795	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
53	50, 51, 52	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
54	53	recnd 10068	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
55	30, 31, 33, 16, 34, 45, 49, 54	fprodsplitsn 14720	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
56	5, 38, 39, 40, 36	hsphoival 40793	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)))
57		iftrue 4092	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
58	57	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
59	56, 58	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (𝐵‘𝑘))
60	59	oveq2d 6666	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
61	60	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
62	61	prodeq2dv 14653	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
63	62	oveq1d 6665	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
64	29, 55, 63	3eqtrd 2660	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
65	28	prodeq1d 14651	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
66		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
67	12	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
68	67, 36	ffvelrnd 6360	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ)
69	59, 42	eqeltrrd 2702	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵‘𝑘) ∈ ℝ)
70		volicore 40795	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
71	68, 69, 70	syl2anc 693	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
72	71	recnd 10068	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
73		fveq2 6191	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (((𝑆‘𝑌)‘𝐴)‘𝐾))
74		fveq2 6191	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐵‘𝑘) = (𝐵‘𝐾))
75	73, 74	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
76	75	fveq2d 6195	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))
77	12, 16	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ)
78	7, 16	ffvelrnd 6360	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ)
79		volicore 40795	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
80	77, 78, 79	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
81	80	recnd 10068	. . . . . 6 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
82	30, 66, 33, 16, 34, 72, 76, 81	fprodsplitsn 14720	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
83	11, 38, 39, 35, 36	hoidifhspval3 40833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))
84		eldifsni 4320	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘 ≠ 𝐾)
85		neneq 2800	. . . . . . . . . . . . 13 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾)
86	84, 85	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
87	86	iffalsed 4097	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
88	87	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
89	83, 88	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (𝐴‘𝑘))
90	89	oveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
91	90	fveq2d 6195	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
92	91	prodeq2dv 14653	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
93	92	oveq1d 6665	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
94	65, 82, 93	3eqtrd 2660	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
95	64, 94	oveq12d 6668	. . 3 ⊢ (𝜑 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
96	28	prodeq1d 14651	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
97		nfcv 2764	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))
98	61, 45	eqeltrrd 2702	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
99	46, 74	oveq12d 6668	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
100	99	fveq2d 6195	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
101		volicore 40795	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
102	50, 78, 101	syl2anc 693	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
103	102	recnd 10068	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
104	30, 97, 33, 16, 34, 98, 100, 103	fprodsplitsn 14720	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
105	96, 104	eqtrd 2656	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
106	5, 6, 3, 7, 16	hsphoival 40793	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
107	34	iffalsed 4097	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
108	106, 107	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
109	108	oveq2d 6666	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)) = ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
110	109	fveq2d 6195	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))))
111	11, 6, 3, 4, 16	hoidifhspval3 40833	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)))
112		eqid 2622	. . . . . . . . . . . 12 ⊢ 𝐾 = 𝐾
113	112	iftruei 4093	. . . . . . . . . . 11 ⊢ if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)
114	113	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
115	111, 114	eqtrd 2656	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
116	115	oveq1d 6665	. . . . . . . 8 ⊢ (𝜑 → ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)) = (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))
117	116	fveq2d 6195	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) = (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))))
118	110, 117	oveq12d 6668	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
119		iftrue 4092	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = (𝐵‘𝐾))
120	119	oveq2d 6666	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
121	120	fveq2d 6195	. . . . . . . . . 10 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
122	121	oveq1d 6665	. . . . . . . . 9 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
123	122	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
124		iftrue 4092	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = (𝐴‘𝐾))
125	124	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
126	125	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
127	78	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
128	6	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
129	50	ad2antrr 762	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
130		simplr 792	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ 𝑌)
131		simpr 477	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
132	127, 128, 129, 130, 131	letrd 10194	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ (𝐴‘𝐾))
133	129	rexrd 10089	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
134	127	rexrd 10089	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ^*)
135		ico0 12221	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
136	133, 134, 135	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
137	132, 136	mpbird 247	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅)
138	126, 137	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
139		iffalse 4095	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = 𝑌)
140	139	oveq1d 6665	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
141	140	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
142		simpr 477	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ≤ 𝑌)
143	6	rexrd 10089	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
144	143	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ^*)
145	78	rexrd 10089	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ^*)
146	145	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ^*)
147		ico0 12221	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
148	144, 146, 147	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
149	142, 148	mpbird 247	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝑌[,)(𝐵‘𝐾)) = ∅)
150	149	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝑌[,)(𝐵‘𝐾)) = ∅)
151	141, 150	eqtrd 2656	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
152	138, 151	pm2.61dan 832	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
153	152	fveq2d 6195	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘∅))
154		vol0 40175	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
155	154	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘∅) = 0)
156	153, 155	eqtrd 2656	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = 0)
157	156	oveq2d 6666	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0))
158	103	addid1d 10236	. . . . . . . . 9 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
159	158	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
160	123, 157, 159	3eqtrd 2660	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
161		iffalse 4095	. . . . . . . . . . . 12 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = 𝑌)
162	161	oveq2d 6666	. . . . . . . . . . 11 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)𝑌))
163	162	fveq2d 6195	. . . . . . . . . 10 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
164	163	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
165	164	oveq1d 6665	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
166		simpl 473	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝜑)
167		simpr 477	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ¬ (𝐵‘𝐾) ≤ 𝑌)
168	166, 6	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
169	166, 78	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ)
170	168, 169	ltnled 10184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝑌 < (𝐵‘𝐾) ↔ ¬ (𝐵‘𝐾) ≤ 𝑌))
171	167, 170	mpbird 247	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 < (𝐵‘𝐾))
172	125	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
173	172	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
174	173	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
175		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
176	50	rexrd 10089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ^*)
177	176	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
178	143	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ^*)
179		ico0 12221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ 𝑌 ∈ ℝ^*) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
180	177, 178, 179	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
181	175, 180	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)𝑌) = ∅)
182	181	fveq2d 6195	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (vol‘∅))
183	154	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘∅) = 0)
184	182, 183	eqtrd 2656	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = 0)
185	184	oveq1d 6665	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
186	185	adantlr 751	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
187	103	addid2d 10237	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
188	187	ad2antrr 762	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
189	174, 186, 188	3eqtrd 2660	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
190	140	fveq2d 6195	. . . . . . . . . . . . 13 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘(𝑌[,)(𝐵‘𝐾))))
191	190	oveq2d 6666	. . . . . . . . . . . 12 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
192	191	adantl 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))))
193		simpl 473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝜑 ∧ 𝑌 < (𝐵‘𝐾)))
194		simpr 477	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ¬ 𝑌 ≤ (𝐴‘𝐾))
195	50	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ)
196	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ)
197	195, 196	ltnled 10184	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴‘𝐾)))
198	194, 197	mpbird 247	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
199	198	adantlr 751	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
200	50	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
201	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
202		volico 40200	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
203	200, 201, 202	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
204		iftrue 4092	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝐾) < 𝑌 → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
205	204	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
206	203, 205	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
207	206	adantlr 751	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
208	6	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → 𝑌 ∈ ℝ)
209	78	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
210		volico 40200	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
211	208, 209, 210	syl2anc 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
212		iftrue 4092	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 < (𝐵‘𝐾) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
213	212	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
214	211, 213	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
215	214	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
216	207, 215	oveq12d 6668	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
217	193, 199, 216	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵‘𝐾)))) = ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)))
218	200	adantlr 751	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
219	208	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
220	209	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐵‘𝐾) ∈ ℝ)
221		simpr 477	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < 𝑌)
222		simplr 792	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 < (𝐵‘𝐾))
223	218, 219, 220, 221, 222	lttrd 10198	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < (𝐵‘𝐾))
224	223	iftrued 4094	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
225	224	eqcomd 2628	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝐵‘𝐾) − (𝐴‘𝐾)) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
226	6, 50	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℝ)
227	226	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℂ)
228	78, 6	resubcld 10458	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℝ)
229	228	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℂ)
230	227, 229	addcomd 10238	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))))
231	78	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℂ)
232	6	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
233	50	recnd 10068	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
234	231, 232, 233	npncand 10416	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
235	230, 234	eqtrd 2656	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
236	235	ad2antrr 762	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
237		volico 40200	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
238	218, 220, 237	syl2anc 693	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
239	225, 236, 238	3eqtr4d 2666	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
240	193, 199, 239	syl2anc 693	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
241	192, 217, 240	3eqtrd 2660	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
242	189, 241	pm2.61dan 832	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
243	166, 171, 242	syl2anc 693	. . . . . . . 8 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
244	165, 243	eqtrd 2656	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
245	160, 244	pm2.61dan 832	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
246	118, 245	eqtr2d 2657	. . . . 5 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
247	246	oveq2d 6666	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
248	33, 98	fprodcl 14682	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
249	248, 54, 81	adddid 10064	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
250	105, 247, 249	3eqtrrd 2661	. . 3 ⊢ (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
251	21, 95, 250	3eqtrd 2660	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
252	2, 3, 18, 4, 7	hoidmvn0val 40798	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
253	252	eqcomd 2628	. 2 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵))
254	15, 251, 253	3eqtrrd 2661	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ≠ wne 2794 ∖ cdif 3571 ∪ cun 3572 ⊆ wss 3574 ∅c0 3915 ifcif 4086 {csn 4177 class class class wbr 4653 ↦ cmpt 4729 ⟶wf 5884 ‘cfv 5888 (class class class)co 6650 ↦ cmpt2 6652 ↑_𝑚 cmap 7857 Fincfn 7955 ℂcc 9934 ℝcr 9935 0cc0 9936 + caddc 9939 · cmul 9941 +∞cpnf 10071 ℝ^*cxr 10073 < clt 10074 ≤ cle 10075 − cmin 10266 +_𝑒 cxad 11944 [,)cico 12177 ∏cprod 14635 volcvol 23232

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-rlim 14220 df-sum 14417 df-prod 14636 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234

This theorem is referenced by: hspmbllem2 40841

W3C validator