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

Theorem hspmbllem1 45215
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
StepHypRef Expression
1 rge0ssre 13420 . . . 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 (𝜑𝐵:𝑋⟶ℝ)
85, 6, 3, 7hsphoif 45165 . . . . 5 (𝜑 → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
92, 3, 4, 8hoidmvcl 45171 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ (0[,)+∞))
101, 9sselid 3978 . . 3 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
1211, 6, 3, 4hoidifhspf 45207 . . . . 5 (𝜑 → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
132, 3, 12, 7hoidmvcl 45171 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ (0[,)+∞))
141, 13sselid 3978 . . 3 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ ℝ)
1510, 14rexaddd 13200 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
16 hspmbllem1.k . . . . . 6 (𝜑𝐾𝑋)
1716ne0d 4333 . . . . 5 (𝜑𝑋 ≠ ∅)
182, 3, 17, 4, 8hoidmvn0val 45173 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
192, 3, 17, 12, 7hoidmvn0val 45173 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
2018, 19oveq12d 7414 . . 3 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))))
21 uncom 4151 . . . . . . . . 9 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
2221a1i 11 . . . . . . . 8 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
2316snssd 4808 . . . . . . . . 9 (𝜑 → {𝐾} ⊆ 𝑋)
24 undif 4479 . . . . . . . . 9 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2523, 24sylib 217 . . . . . . . 8 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2622, 25eqtrd 2773 . . . . . . 7 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
2726eqcomd 2739 . . . . . 6 (𝜑𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
2827prodeq1d 15852 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
29 nfv 1918 . . . . . 6 𝑘𝜑
30 nfcv 2904 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
31 difssd 4130 . . . . . . 7 (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
323, 31ssfid 9255 . . . . . 6 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33 neldifsnd 4792 . . . . . 6 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
344adantr 482 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
3531sselda 3980 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘𝑋)
3634, 35ffvelcdmd 7075 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴𝑘) ∈ ℝ)
376adantr 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
383adantr 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
397adantr 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
405, 37, 38, 39hsphoif 45165 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
4140, 35ffvelcdmd 7075 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42 volicore 45170 . . . . . . . 8 (((𝐴𝑘) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4336, 41, 42syl2anc 585 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4443recnd 11229 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45 fveq2 6881 . . . . . . . 8 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
46 fveq2 6881 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑇𝑌)‘𝐵)‘𝑘) = (((𝑇𝑌)‘𝐵)‘𝐾))
4745, 46oveq12d 7414 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
4847fveq2d 6885 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))))
494, 16ffvelcdmd 7075 . . . . . . . 8 (𝜑 → (𝐴𝐾) ∈ ℝ)
508, 16ffvelcdmd 7075 . . . . . . . 8 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51 volicore 45170 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5249, 50, 51syl2anc 585 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5352recnd 11229 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
5429, 30, 32, 16, 33, 44, 48, 53fprodsplitsn 15920 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
555, 37, 38, 39, 35hsphoival 45168 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)))
56 iftrue 4530 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5756adantl 483 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5855, 57eqtrd 2773 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = (𝐵𝑘))
5958oveq2d 7412 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
6059fveq2d 6885 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6160prodeq2dv 15854 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6261oveq1d 7411 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6328, 54, 623eqtrd 2777 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6427prodeq1d 15852 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
65 nfcv 2904 . . . . . 6 𝑘(vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
6612adantr 482 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
6766, 35ffvelcdmd 7075 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ)
6858, 41eqeltrrd 2835 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵𝑘) ∈ ℝ)
69 volicore 45170 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7067, 68, 69syl2anc 585 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7170recnd 11229 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℂ)
72 fveq2 6881 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑆𝑌)‘𝐴)‘𝑘) = (((𝑆𝑌)‘𝐴)‘𝐾))
73 fveq2 6881 . . . . . . . 8 (𝑘 = 𝐾 → (𝐵𝑘) = (𝐵𝐾))
7472, 73oveq12d 7414 . . . . . . 7 (𝑘 = 𝐾 → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
7574fveq2d 6885 . . . . . 6 (𝑘 = 𝐾 → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))
7612, 16ffvelcdmd 7075 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ)
777, 16ffvelcdmd 7075 . . . . . . . 8 (𝜑 → (𝐵𝐾) ∈ ℝ)
78 volicore 45170 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
7976, 77, 78syl2anc 585 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8079recnd 11229 . . . . . 6 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℂ)
8129, 65, 32, 16, 33, 71, 75, 80fprodsplitsn 15920 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
8211, 37, 38, 34, 35hoidifhspval3 45208 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)))
83 eldifsni 4789 . . . . . . . . . . . 12 (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘𝐾)
84 neneq 2947 . . . . . . . . . . . 12 (𝑘𝐾 → ¬ 𝑘 = 𝐾)
8583, 84syl 17 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
8685iffalsed 4535 . . . . . . . . . 10 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8786adantl 483 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8882, 87eqtrd 2773 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = (𝐴𝑘))
8988fvoveq1d 7418 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9089prodeq2dv 15854 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9190oveq1d 7411 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9264, 81, 913eqtrd 2777 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9363, 92oveq12d 7414 . . 3 (𝜑 → (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
9427prodeq1d 15852 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
95 nfcv 2904 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(𝐵𝐾)))
9660, 44eqeltrrd 2835 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
9745, 73oveq12d 7414 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝐾)[,)(𝐵𝐾)))
9897fveq2d 6885 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
99 volicore 45170 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
10049, 77, 99syl2anc 585 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
101100recnd 11229 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℂ)
10229, 95, 32, 16, 33, 96, 98, 101fprodsplitsn 15920 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
10394, 102eqtrd 2773 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
1045, 6, 3, 7, 16hsphoival 45168 . . . . . . . . . 10 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
10533iffalsed 4535 . . . . . . . . . 10 (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
106104, 105eqtrd 2773 . . . . . . . . 9 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
107106oveq2d 7412 . . . . . . . 8 (𝜑 → ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)) = ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
108107fveq2d 6885 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))))
10911, 6, 3, 4, 16hoidifhspval3 45208 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)))
110 eqid 2733 . . . . . . . . . . 11 𝐾 = 𝐾
111110iftruei 4531 . . . . . . . . . 10 if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)
112111a1i 11 . . . . . . . . 9 (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
113109, 112eqtrd 2773 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
114113fvoveq1d 7418 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) = (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))))
115108, 114oveq12d 7414 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
116 iftrue 4530 . . . . . . . . . . . 12 ((𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = (𝐵𝐾))
117116oveq2d 7412 . . . . . . . . . . 11 ((𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)(𝐵𝐾)))
118117fveq2d 6885 . . . . . . . . . 10 ((𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
119118oveq1d 7411 . . . . . . . . 9 ((𝐵𝐾) ≤ 𝑌 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
120119adantl 483 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
121 iftrue 4530 . . . . . . . . . . . . . . 15 (𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = (𝐴𝐾))
122121oveq1d 7411 . . . . . . . . . . . . . 14 (𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
123122adantl 483 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
12477ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ)
1256ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
12649ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
127 simplr 768 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ 𝑌)
128 simpr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
129124, 125, 126, 127, 128letrd 11358 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ (𝐴𝐾))
130126rexrd 11251 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
131124rexrd 11251 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ*)
132 ico0 13357 . . . . . . . . . . . . . . 15 (((𝐴𝐾) ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
133130, 131, 132syl2anc 585 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
134129, 133mpbird 257 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)(𝐵𝐾)) = ∅)
135123, 134eqtrd 2773 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
136 iffalse 4533 . . . . . . . . . . . . . . 15 𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = 𝑌)
137136oveq1d 7411 . . . . . . . . . . . . . 14 𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
138137adantl 483 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
139 simpr 486 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ≤ 𝑌)
1406rexrd 11251 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ ℝ*)
141140adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ*)
14277rexrd 11251 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐾) ∈ ℝ*)
143142adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ*)
144 ico0 13357 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
145141, 143, 144syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
146139, 145mpbird 257 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝑌[,)(𝐵𝐾)) = ∅)
147146adantr 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝑌[,)(𝐵𝐾)) = ∅)
148138, 147eqtrd 2773 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
149135, 148pm2.61dan 812 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
150149fveq2d 6885 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘∅))
151 vol0 44548 . . . . . . . . . . 11 (vol‘∅) = 0
152151a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153150, 152eqtrd 2773 . . . . . . . . 9 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = 0)
154153oveq2d 7412 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0))
155101addridd 11401 . . . . . . . . 9 (𝜑 → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
156155adantr 482 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
157120, 154, 1563eqtrd 2777 . . . . . . 7 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
158 iffalse 4533 . . . . . . . . . . . 12 (¬ (𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = 𝑌)
159158oveq2d 7412 . . . . . . . . . . 11 (¬ (𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)𝑌))
160159fveq2d 6885 . . . . . . . . . 10 (¬ (𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
161160adantl 483 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
162161oveq1d 7411 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
163 simpl 484 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝜑)
164 simpr 486 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ¬ (𝐵𝐾) ≤ 𝑌)
165163, 6syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
166163, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ)
167165, 166ltnled 11348 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝑌 < (𝐵𝐾) ↔ ¬ (𝐵𝐾) ≤ 𝑌))
168164, 167mpbird 257 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 < (𝐵𝐾))
169121fvoveq1d 7418 . . . . . . . . . . . . 13 (𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
170169oveq2d 7412 . . . . . . . . . . . 12 (𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
171170adantl 483 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
172 simpr 486 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
17349rexrd 11251 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐾) ∈ ℝ*)
174173adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
175140adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ*)
176 ico0 13357 . . . . . . . . . . . . . . . . 17 (((𝐴𝐾) ∈ ℝ*𝑌 ∈ ℝ*) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
177174, 175, 176syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
178172, 177mpbird 257 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)𝑌) = ∅)
179178fveq2d 6885 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = (vol‘∅))
180151a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘∅) = 0)
181179, 180eqtrd 2773 . . . . . . . . . . . . 13 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = 0)
182181oveq1d 7411 . . . . . . . . . . . 12 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
183182adantlr 714 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
184101addlidd 11402 . . . . . . . . . . . 12 (𝜑 → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
185184ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
186171, 183, 1853eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
187136fvoveq1d 7418 . . . . . . . . . . . . 13 𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘(𝑌[,)(𝐵𝐾))))
188187oveq2d 7412 . . . . . . . . . . . 12 𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
189188adantl 483 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
190 simpl 484 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝜑𝑌 < (𝐵𝐾)))
191 simpr 486 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ¬ 𝑌 ≤ (𝐴𝐾))
19249adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
1936adantr 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
194192, 193ltnled 11348 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴𝐾)))
195191, 194mpbird 257 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
196195adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
19749adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
1986adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199 volico 44572 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
200197, 198, 199syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
201 iftrue 4530 . . . . . . . . . . . . . . . 16 ((𝐴𝐾) < 𝑌 → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
202201adantl 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
203200, 202eqtrd 2773 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
204203adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
2056adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → 𝑌 ∈ ℝ)
20677adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → (𝐵𝐾) ∈ ℝ)
207 volico 44572 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
208205, 206, 207syl2anc 585 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
209 iftrue 4530 . . . . . . . . . . . . . . . 16 (𝑌 < (𝐵𝐾) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
210209adantl 483 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
211208, 210eqtrd 2773 . . . . . . . . . . . . . 14 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
212211adantr 482 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
213204, 212oveq12d 7414 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
214190, 196, 213syl2anc 585 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
215197adantlr 714 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
216205adantr 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
217206adantr 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐵𝐾) ∈ ℝ)
218 simpr 486 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < 𝑌)
219 simplr 768 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 < (𝐵𝐾))
220215, 216, 217, 218, 219lttrd 11362 . . . . . . . . . . . . . . 15 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < (𝐵𝐾))
221220iftrued 4532 . . . . . . . . . . . . . 14 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0) = ((𝐵𝐾) − (𝐴𝐾)))
222221eqcomd 2739 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝐵𝐾) − (𝐴𝐾)) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
2236, 49resubcld 11629 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℝ)
224223recnd 11229 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℂ)
22577, 6resubcld 11629 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℝ)
226225recnd 11229 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℂ)
227224, 226addcomd 11403 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))))
22877recnd 11229 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐾) ∈ ℂ)
2296recnd 11229 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
23049recnd 11229 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐾) ∈ ℂ)
231228, 229, 230npncand 11582 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))) = ((𝐵𝐾) − (𝐴𝐾)))
232227, 231eqtrd 2773 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
233232ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
234 volico 44572 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
235215, 217, 234syl2anc 585 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
236222, 233, 2353eqtr4d 2783 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
237190, 196, 236syl2anc 585 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
238189, 214, 2373eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
239186, 238pm2.61dan 812 . . . . . . . . 9 ((𝜑𝑌 < (𝐵𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
240163, 168, 239syl2anc 585 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
241162, 240eqtrd 2773 . . . . . . 7 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
242157, 241pm2.61dan 812 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
243115, 242eqtr2d 2774 . . . . 5 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
244243oveq2d 7412 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
24532, 96fprodcl 15883 . . . . 5 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
246245, 53, 80adddid 11225 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
247103, 244, 2463eqtrrd 2778 . . 3 (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24820, 93, 2473eqtrd 2777 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
2492, 3, 17, 4, 7hoidmvn0val 45173 . . 3 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
250249eqcomd 2739 . 2 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (𝐴(𝐿𝑋)𝐵))
25115, 248, 2503eqtrrd 2778 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wne 2941  cdif 3943  cun 3944  wss 3946  c0 4320  ifcif 4524  {csn 4624   class class class wbr 5144  cmpt 5227  wf 6531  cfv 6535  (class class class)co 7396  cmpo 7398  m cmap 8808  Fincfn 8927  cc 11095  cr 11096  0cc0 11097   + caddc 11100   · cmul 11102  +∞cpnf 11232  *cxr 11234   < clt 11235  cle 11236  cmin 11431   +𝑒 cxad 13077  [,)cico 13313  cprod 15836  volcvol 24949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5359  ax-pr 5423  ax-un 7712  ax-inf2 9623  ax-cnex 11153  ax-resscn 11154  ax-1cn 11155  ax-icn 11156  ax-addcl 11157  ax-addrcl 11158  ax-mulcl 11159  ax-mulrcl 11160  ax-mulcom 11161  ax-addass 11162  ax-mulass 11163  ax-distr 11164  ax-i2m1 11165  ax-1ne0 11166  ax-1rid 11167  ax-rnegex 11168  ax-rrecex 11169  ax-cnre 11170  ax-pre-lttri 11171  ax-pre-lttrn 11172  ax-pre-ltadd 11173  ax-pre-mulgt0 11174  ax-pre-sup 11175
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4905  df-int 4947  df-iun 4995  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6292  df-ord 6359  df-on 6360  df-lim 6361  df-suc 6362  df-iota 6487  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-isom 6544  df-riota 7352  df-ov 7399  df-oprab 7400  df-mpo 7401  df-of 7657  df-om 7843  df-1st 7962  df-2nd 7963  df-frecs 8253  df-wrecs 8284  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8691  df-map 8810  df-pm 8811  df-en 8928  df-dom 8929  df-sdom 8930  df-fin 8931  df-fi 9393  df-sup 9424  df-inf 9425  df-oi 9492  df-dju 9883  df-card 9921  df-pnf 11237  df-mnf 11238  df-xr 11239  df-ltxr 11240  df-le 11241  df-sub 11433  df-neg 11434  df-div 11859  df-nn 12200  df-2 12262  df-3 12263  df-n0 12460  df-z 12546  df-uz 12810  df-q 12920  df-rp 12962  df-xneg 13079  df-xadd 13080  df-xmul 13081  df-ioo 13315  df-ico 13317  df-icc 13318  df-fz 13472  df-fzo 13615  df-fl 13744  df-seq 13954  df-exp 14015  df-hash 14278  df-cj 15033  df-re 15034  df-im 15035  df-sqrt 15169  df-abs 15170  df-clim 15419  df-rlim 15420  df-sum 15620  df-prod 15837  df-rest 17355  df-topgen 17376  df-psmet 20910  df-xmet 20911  df-met 20912  df-bl 20913  df-mopn 20914  df-top 22365  df-topon 22382  df-bases 22418  df-cmp 22860  df-ovol 24950  df-vol 24951
This theorem is referenced by:  hspmbllem2  45216
  Copyright terms: Public domain W3C validator