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 47605

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 13580	. . . 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 47555	. . . . 5 ⊢ (𝜑 → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
9	2, 3, 4, 8	hoidmvcl 47561	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ (0[,)+∞))
10	1, 9	sselid 3929	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) ∈ ℝ)
11		hspmbllem1.s	. . . . . 6 ⊢ 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑_m 𝑋) ↦ (ℎ ∈ 𝑋 ↦ if(ℎ = 𝐾, if(𝑥 ≤ (𝑐‘ℎ), (𝑐‘ℎ), 𝑥), (𝑐‘ℎ)))))
12	11, 6, 3, 4	hoidifhspf 47597	. . . . 5 ⊢ (𝜑 → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
13	2, 3, 12, 7	hoidmvcl 47561	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ (0[,)+∞))
14	1, 13	sselid 3929	. . 3 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) ∈ ℝ)
15	10, 14	rexaddd 13357	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))
16		hspmbllem1.k	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
17	16	ne0d 4288	. . . . 5 ⊢ (𝜑 → 𝑋 ≠ ∅)
18	2, 3, 17, 4, 8	hoidmvn0val 47563	. . . 4 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
19	2, 3, 17, 12, 7	hoidmvn0val 47563	. . . 4 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
20	18, 19	oveq12d 7436	. . 3 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))))
21		uncom 4105	. . . . . . . . 9 ⊢ ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
22	21	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
23	16	snssd 4747	. . . . . . . . 9 ⊢ (𝜑 → {𝐾} ⊆ 𝑋)
24		undif 4438	. . . . . . . . 9 ⊢ ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
25	23, 24	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
26	22, 25	eqtrd 2796	. . . . . . 7 ⊢ (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
27	26	eqcomd 2767	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
28	27	prodeq1d 16081	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))))
29		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑘𝜑
30		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
31		difssd 4084	. . . . . . 7 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
32	3, 31	ssfid 9253	. . . . . 6 ⊢ (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33		neldifsnd 4756	. . . . . 6 ⊢ (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
34	4	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
35	31	sselda 3931	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘 ∈ 𝑋)
36	34, 35	ffvelcdmd 7083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴‘𝑘) ∈ ℝ)
37	6	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
38	3	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
39	7	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
40	5, 37, 38, 39	hsphoif 47555	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇‘𝑌)‘𝐵):𝑋⟶ℝ)
41	40, 35	ffvelcdmd 7083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42		volicore 47560	. . . . . . . 8 ⊢ (((𝐴‘𝑘) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
43	36, 41, 42	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
44	43	recnd 11330	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45		fveq2 6883	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾))
46		fveq2 6883	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (((𝑇‘𝑌)‘𝐵)‘𝐾))
47	45, 46	oveq12d 7436	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))
48	47	fveq2d 6887	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))))
49	4, 16	ffvelcdmd 7083	. . . . . . . 8 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ)
50	8, 16	ffvelcdmd 7083	. . . . . . . 8 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51		volicore 47560	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (((𝑇‘𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
52	49, 50, 51	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
53	52	recnd 11330	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
54	29, 30, 32, 16, 33, 44, 48, 53	fprodsplitsn 16149	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
55	5, 37, 38, 39, 35	hsphoival 47558	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)))
56		iftrue 4488	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
57	56	adantl 487	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝑘), if((𝐵‘𝑘) ≤ 𝑌, (𝐵‘𝑘), 𝑌)) = (𝐵‘𝑘))
58	55, 57	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇‘𝑌)‘𝐵)‘𝑘) = (𝐵‘𝑘))
59	58	oveq2d 7434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘)) = ((𝐴‘𝑘)[,)(𝐵‘𝑘)))
60	59	fveq2d 6887	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
61	60	prodeq2dv 16083	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
62	61	oveq1d 7433	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
63	28, 54, 62	3eqtrd 2800	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))))
64	27	prodeq1d 16081	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))))
65		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
66	12	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆‘𝑌)‘𝐴):𝑋⟶ℝ)
67	66, 35	ffvelcdmd 7083	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ)
68	58, 41	eqeltrrd 2862	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵‘𝑘) ∈ ℝ)
69		volicore 47560	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵‘𝑘) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
70	67, 68, 69	syl2anc 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℝ)
71	70	recnd 11330	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
72		fveq2 6883	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (((𝑆‘𝑌)‘𝐴)‘𝐾))
73		fveq2 6883	. . . . . . . 8 ⊢ (𝑘 = 𝐾 → (𝐵‘𝑘) = (𝐵‘𝐾))
74	72, 73	oveq12d 7436	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)) = ((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))
75	74	fveq2d 6887	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))
76	12, 16	ffvelcdmd 7083	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ)
77	7, 16	ffvelcdmd 7083	. . . . . . . 8 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ)
78		volicore 47560	. . . . . . . 8 ⊢ (((((𝑆‘𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
79	76, 77, 78	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
80	79	recnd 11330	. . . . . 6 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
81	29, 65, 32, 16, 33, 71, 75, 80	fprodsplitsn 16149	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
82	11, 37, 38, 34, 35	hoidifhspval3 47598	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)))
83		eldifsni 4753	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘 ≠ 𝐾)
84		neneq 2962	. . . . . . . . . . . 12 ⊢ (𝑘 ≠ 𝐾 → ¬ 𝑘 = 𝐾)
85	83, 84	syl 18	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
86	85	iffalsed 4493	. . . . . . . . . 10 ⊢ (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
87	86	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴‘𝑘), (𝐴‘𝑘), 𝑌), (𝐴‘𝑘)) = (𝐴‘𝑘))
88	82, 87	eqtrd 2796	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆‘𝑌)‘𝐴)‘𝑘) = (𝐴‘𝑘))
89	88	fvoveq1d 7440	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
90	89	prodeq2dv 16083	. . . . . 6 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
91	90	oveq1d 7433	. . . . 5 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
92	64, 81, 91	3eqtrd 2800	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
93	63, 92	oveq12d 7436	. . 3 ⊢ (𝜑 → (∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(((𝑇‘𝑌)‘𝐵)‘𝑘))) + ∏𝑘 ∈ 𝑋 (vol‘((((𝑆‘𝑌)‘𝐴)‘𝑘)[,)(𝐵‘𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
94	27	prodeq1d 16081	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
95		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑘(vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))
96	60, 44	eqeltrrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
97	45, 73	oveq12d 7436	. . . . . . 7 ⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘)[,)(𝐵‘𝑘)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
98	97	fveq2d 6887	. . . . . 6 ⊢ (𝑘 = 𝐾 → (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
99		volicore 47560	. . . . . . . 8 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
100	49, 77, 99	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℝ)
101	100	recnd 11330	. . . . . 6 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) ∈ ℂ)
102	29, 95, 32, 16, 33, 96, 98, 101	fprodsplitsn 16149	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
103	94, 102	eqtrd 2796	. . . 4 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
104	5, 6, 3, 7, 16	hsphoival 47558	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
105	33	iffalsed 4493	. . . . . . . . . 10 ⊢ (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵‘𝐾), if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
106	104, 105	eqtrd 2796	. . . . . . . . 9 ⊢ (𝜑 → (((𝑇‘𝑌)‘𝐵)‘𝐾) = if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))
107	106	oveq2d 7434	. . . . . . . 8 ⊢ (𝜑 → ((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)) = ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)))
108	107	fveq2d 6887	. . . . . . 7 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))))
109	11, 6, 3, 4, 16	hoidifhspval3 47598	. . . . . . . . 9 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)))
110		eqid 2761	. . . . . . . . . . 11 ⊢ 𝐾 = 𝐾
111	110	iftruei 4489	. . . . . . . . . 10 ⊢ if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)
112	111	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌), (𝐴‘𝐾)) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
113	109, 112	eqtrd 2796	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌))
114	113	fvoveq1d 7440	. . . . . . 7 ⊢ (𝜑 → (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))) = (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))))
115	108, 114	oveq12d 7436	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
116		iftrue 4488	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = (𝐵‘𝐾))
117	116	oveq2d 7434	. . . . . . . . . . 11 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)(𝐵‘𝐾)))
118	117	fveq2d 6887	. . . . . . . . . 10 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
119	118	oveq1d 7433	. . . . . . . . 9 ⊢ ((𝐵‘𝐾) ≤ 𝑌 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
120	119	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))))
121		iftrue 4488	. . . . . . . . . . . . . . 15 ⊢ (𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = (𝐴‘𝐾))
122	121	oveq1d 7433	. . . . . . . . . . . . . 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 11460	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ≤ (𝐴‘𝐾))
130	126	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
131	124	rexrd 11352	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐵‘𝐾) ∈ ℝ^*)
132		ico0 13515	. . . . . . . . . . . . . . 15 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
133	130, 131, 132	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ (𝐴‘𝐾)))
134	129, 133	mpbird 260	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)(𝐵‘𝐾)) = ∅)
135	123, 134	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
136		iffalse 4491	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌) = 𝑌)
137	136	oveq1d 7433	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
138	137	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = (𝑌[,)(𝐵‘𝐾)))
139		simpr 490	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ≤ 𝑌)
140	6	rexrd 11352	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ ℝ^*)
141	140	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ^*)
142	77	rexrd 11352	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℝ^*)
143	142	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝐵‘𝐾) ∈ ℝ^*)
144		ico0 13515	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ^* ∧ (𝐵‘𝐾) ∈ ℝ^*) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
145	141, 143, 144	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵‘𝐾)) = ∅ ↔ (𝐵‘𝐾) ≤ 𝑌))
146	139, 145	mpbird 260	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (𝑌[,)(𝐵‘𝐾)) = ∅)
147	146	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝑌[,)(𝐵‘𝐾)) = ∅)
148	138, 147	eqtrd 2796	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
149	135, 148	pm2.61dan 825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)) = ∅)
150	149	fveq2d 6887	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘∅))
151		vol0 46938	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
152	151	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153	150, 152	eqtrd 2796	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = 0)
154	153	oveq2d 7434	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0))
155	101	addridd 11503	. . . . . . . . 9 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
156	155	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) + 0) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
157	120, 154, 156	3eqtrd 2800	. . . . . . 7 ⊢ ((𝜑 ∧ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
158		iffalse 4491	. . . . . . . . . . . 12 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌) = 𝑌)
159	158	oveq2d 7434	. . . . . . . . . . 11 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → ((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌)) = ((𝐴‘𝐾)[,)𝑌))
160	159	fveq2d 6887	. . . . . . . . . 10 ⊢ (¬ (𝐵‘𝐾) ≤ 𝑌 → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
161	160	adantl 487	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) = (vol‘((𝐴‘𝐾)[,)𝑌)))
162	161	oveq1d 7433	. . . . . . . 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 11450	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → (𝑌 < (𝐵‘𝐾) ↔ ¬ (𝐵‘𝐾) ≤ 𝑌))
168	164, 167	mpbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → 𝑌 < (𝐵‘𝐾))
169	121	fvoveq1d 7440	. . . . . . . . . . . . 13 ⊢ (𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
170	169	oveq2d 7434	. . . . . . . . . . . 12 ⊢ (𝑌 ≤ (𝐴‘𝐾) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
171	170	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
172		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ≤ (𝐴‘𝐾))
173	49	rexrd 11352	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℝ^*)
174	173	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) ∈ ℝ^*)
175	140	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → 𝑌 ∈ ℝ^*)
176		ico0 13515	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴‘𝐾) ∈ ℝ^* ∧ 𝑌 ∈ ℝ^*) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
177	174, 175, 176	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (((𝐴‘𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴‘𝐾)))
178	172, 177	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾)[,)𝑌) = ∅)
179	178	fveq2d 6887	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (vol‘∅))
180	151	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘∅) = 0)
181	179, 180	eqtrd 2796	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → (vol‘((𝐴‘𝐾)[,)𝑌)) = 0)
182	181	oveq1d 7433	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
183	182	adantlr 728	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))))
184	101	addlidd 11504	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
185	184	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → (0 + (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
186	171, 183, 185	3eqtrd 2800	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ 𝑌 ≤ (𝐴‘𝐾)) → ((vol‘((𝐴‘𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
187	136	fvoveq1d 7440	. . . . . . . . . . . . 13 ⊢ (¬ 𝑌 ≤ (𝐴‘𝐾) → (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾))) = (vol‘(𝑌[,)(𝐵‘𝐾))))
188	187	oveq2d 7434	. . . . . . . . . . . 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 11450	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝐴‘𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴‘𝐾)))
195	191, 194	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
196	195	adantlr 728	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → (𝐴‘𝐾) < 𝑌)
197	49	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) ∈ ℝ)
198	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199		volico 46962	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
200	197, 198, 199	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0))
201		iftrue 4488	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴‘𝐾) < 𝑌 → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
202	201	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < 𝑌, (𝑌 − (𝐴‘𝐾)), 0) = (𝑌 − (𝐴‘𝐾)))
203	200, 202	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
204	203	adantlr 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)𝑌)) = (𝑌 − (𝐴‘𝐾)))
205	6	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → 𝑌 ∈ ℝ)
206	77	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (𝐵‘𝐾) ∈ ℝ)
207		volico 46962	. . . . . . . . . . . . . . . 16 ⊢ ((𝑌 ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
208	205, 206, 207	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0))
209		iftrue 4488	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 < (𝐵‘𝐾) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
210	209	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → if(𝑌 < (𝐵‘𝐾), ((𝐵‘𝐾) − 𝑌), 0) = ((𝐵‘𝐾) − 𝑌))
211	208, 210	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
212	211	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵‘𝐾))) = ((𝐵‘𝐾) − 𝑌))
213	204, 212	oveq12d 7436	. . . . . . . . . . . 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 11464	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (𝐴‘𝐾) < (𝐵‘𝐾))
221	220	iftrued 4490	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
222	221	eqcomd 2767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝐵‘𝐾) − (𝐴‘𝐾)) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
223	6, 49	resubcld 11737	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℝ)
224	223	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑌 − (𝐴‘𝐾)) ∈ ℂ)
225	77, 6	resubcld 11737	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℝ)
226	225	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵‘𝐾) − 𝑌) ∈ ℂ)
227	224, 226	addcomd 11505	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))))
228	77	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵‘𝐾) ∈ ℂ)
229	6	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ ℂ)
230	49	recnd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴‘𝐾) ∈ ℂ)
231	228, 229, 230	npncand 11686	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐵‘𝐾) − 𝑌) + (𝑌 − (𝐴‘𝐾))) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
232	227, 231	eqtrd 2796	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
233	232	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = ((𝐵‘𝐾) − (𝐴‘𝐾)))
234		volico 46962	. . . . . . . . . . . . . 14 ⊢ (((𝐴‘𝐾) ∈ ℝ ∧ (𝐵‘𝐾) ∈ ℝ) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
235	215, 217, 234	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = if((𝐴‘𝐾) < (𝐵‘𝐾), ((𝐵‘𝐾) − (𝐴‘𝐾)), 0))
236	222, 233, 235	3eqtr4d 2806	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ (𝐴‘𝐾) < 𝑌) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
237	190, 196, 236	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑌 < (𝐵‘𝐾)) ∧ ¬ 𝑌 ≤ (𝐴‘𝐾)) → ((𝑌 − (𝐴‘𝐾)) + ((𝐵‘𝐾) − 𝑌)) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
238	189, 214, 237	3eqtrd 2800	. . . . . . . . . 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 2796	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐵‘𝐾) ≤ 𝑌) → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
242	157, 241	pm2.61dan 825	. . . . . 6 ⊢ (𝜑 → ((vol‘((𝐴‘𝐾)[,)if((𝐵‘𝐾) ≤ 𝑌, (𝐵‘𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴‘𝐾), (𝐴‘𝐾), 𝑌)[,)(𝐵‘𝐾)))) = (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))))
243	115, 242	eqtr2d 2797	. . . . 5 ⊢ (𝜑 → (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾))) = ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾)))))
244	243	oveq2d 7434	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(𝐵‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
245	32, 96	fprodcl 16112	. . . . 5 ⊢ (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) ∈ ℂ)
246	245, 53, 80	adddid 11326	. . . 4 ⊢ (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · ((vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))))
247	103, 244, 246	3eqtrrd 2801	. . 3 ⊢ (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((𝐴‘𝐾)[,)(((𝑇‘𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) · (vol‘((((𝑆‘𝑌)‘𝐴)‘𝐾)[,)(𝐵‘𝐾))))) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
248	20, 93, 247	3eqtrd 2800	. 2 ⊢ (𝜑 → ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) + (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
249	2, 3, 17, 4, 7	hoidmvn0val 47563	. . 3 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))))
250	249	eqcomd 2767	. 2 ⊢ (𝜑 → ∏𝑘 ∈ 𝑋 (vol‘((𝐴‘𝑘)[,)(𝐵‘𝑘))) = (𝐴(𝐿‘𝑋)𝐵))
251	15, 248, 250	3eqtrrd 2801	1 ⊢ (𝜑 → (𝐴(𝐿‘𝑋)𝐵) = ((𝐴(𝐿‘𝑋)((𝑇‘𝑌)‘𝐵)) +_𝑒 (((𝑆‘𝑌)‘𝐴)(𝐿‘𝑋)𝐵)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∖ cdif 3896 ∪ cun 3897 ⊆ wss 3899 ∅c0 4279 ifcif 4482 {csn 4584 class class class wbr 5103 ↦ cmpt 5186 ⟶wf 6533 ‘cfv 6537 (class class class)co 7418 ∈ cmpo 7420 ↑_m cmap 8840 Fincfn 8966 ℂcc 11191 ℝcr 11192 0cc0 11193 + caddc 11196 · cmul 11198 +∞cpnf 11333 ℝ^*cxr 11335 < clt 11336 ≤ cle 11337 − cmin 11534 +_𝑒 cxad 13232 [,)cico 13471 ∏cprod 16065 volcvol 25777

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271

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 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-dju 9975 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-n0 12600 df-z 12687 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-seq 14138 df-exp 14198 df-hash 14468 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-clim 15648 df-rlim 15649 df-sum 15847 df-prod 16066 df-rest 17586 df-topgen 17607 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-top 23205 df-topon 23222 df-bases 23257 df-cmp 23698 df-ovol 25778 df-vol 25779

This theorem is used by: hspmbllem2 47606

W3C validator