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 39310
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
StepHypRef Expression
1 rge0ssre 12110 . . . 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 (𝜑𝐵:𝑋⟶ℝ)
85, 6, 3, 7hsphoif 39260 . . . . 5 (𝜑 → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
92, 3, 4, 8hoidmvcl 39266 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ (0[,)+∞))
101, 9sseldi 3566 . . 3 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
1211, 6, 3, 4hoidifhspf 39302 . . . . 5 (𝜑 → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
132, 3, 12, 7hoidmvcl 39266 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ (0[,)+∞))
141, 13sseldi 3566 . . 3 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ ℝ)
1510, 14rexaddd 11901 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
16 hspmbllem1.k . . . . . 6 (𝜑𝐾𝑋)
17 ne0i 3880 . . . . . 6 (𝐾𝑋𝑋 ≠ ∅)
1816, 17syl 17 . . . . 5 (𝜑𝑋 ≠ ∅)
192, 3, 18, 4, 8hoidmvn0val 39268 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
202, 3, 18, 12, 7hoidmvn0val 39268 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
2119, 20oveq12d 6545 . . 3 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))))
22 uncom 3719 . . . . . . . . 9 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
2322a1i 11 . . . . . . . 8 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
2416snssd 4281 . . . . . . . . 9 (𝜑 → {𝐾} ⊆ 𝑋)
25 undif 4001 . . . . . . . . 9 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2624, 25sylib 207 . . . . . . . 8 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2723, 26eqtrd 2644 . . . . . . 7 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
2827eqcomd 2616 . . . . . 6 (𝜑𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
2928prodeq1d 14439 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
30 nfv 1830 . . . . . 6 𝑘𝜑
31 nfcv 2751 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
32 difssd 3700 . . . . . . 7 (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
333, 32ssfid 8046 . . . . . 6 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
34 neldifsnd 4263 . . . . . 6 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
354adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
3632sselda 3568 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘𝑋)
3735, 36ffvelrnd 6253 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴𝑘) ∈ ℝ)
386adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
393adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
407adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
415, 38, 39, 40hsphoif 39260 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
4241, 36ffvelrnd 6253 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ)
43 volicore 39265 . . . . . . . 8 (((𝐴𝑘) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4437, 42, 43syl2anc 691 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4544recnd 9925 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
46 fveq2 6088 . . . . . . . 8 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
47 fveq2 6088 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑇𝑌)‘𝐵)‘𝑘) = (((𝑇𝑌)‘𝐵)‘𝐾))
4846, 47oveq12d 6545 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
4948fveq2d 6092 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))))
504, 16ffvelrnd 6253 . . . . . . . 8 (𝜑 → (𝐴𝐾) ∈ ℝ)
518, 16ffvelrnd 6253 . . . . . . . 8 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ)
52 volicore 39265 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5350, 51, 52syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5453recnd 9925 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
5530, 31, 33, 16, 34, 45, 49, 54fprodsplitsn 14508 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
565, 38, 39, 40, 36hsphoival 39263 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)))
57 iftrue 4042 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5857adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5956, 58eqtrd 2644 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = (𝐵𝑘))
6059oveq2d 6543 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
6160fveq2d 6092 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6261prodeq2dv 14441 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6362oveq1d 6542 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6429, 55, 633eqtrd 2648 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6528prodeq1d 14439 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
66 nfcv 2751 . . . . . 6 𝑘(vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
6712adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
6867, 36ffvelrnd 6253 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ)
6959, 42eqeltrrd 2689 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵𝑘) ∈ ℝ)
70 volicore 39265 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7168, 69, 70syl2anc 691 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7271recnd 9925 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℂ)
73 fveq2 6088 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑆𝑌)‘𝐴)‘𝑘) = (((𝑆𝑌)‘𝐴)‘𝐾))
74 fveq2 6088 . . . . . . . 8 (𝑘 = 𝐾 → (𝐵𝑘) = (𝐵𝐾))
7573, 74oveq12d 6545 . . . . . . 7 (𝑘 = 𝐾 → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
7675fveq2d 6092 . . . . . 6 (𝑘 = 𝐾 → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))
7712, 16ffvelrnd 6253 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ)
787, 16ffvelrnd 6253 . . . . . . . 8 (𝜑 → (𝐵𝐾) ∈ ℝ)
79 volicore 39265 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8077, 78, 79syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8180recnd 9925 . . . . . 6 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℂ)
8230, 66, 33, 16, 34, 72, 76, 81fprodsplitsn 14508 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
8311, 38, 39, 35, 36hoidifhspval3 39303 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)))
84 eldifsni 4261 . . . . . . . . . . . . 13 (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘𝐾)
85 neneq 2788 . . . . . . . . . . . . 13 (𝑘𝐾 → ¬ 𝑘 = 𝐾)
8684, 85syl 17 . . . . . . . . . . . 12 (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
8786iffalsed 4047 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8887adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8983, 88eqtrd 2644 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = (𝐴𝑘))
9089oveq1d 6542 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
9190fveq2d 6092 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9291prodeq2dv 14441 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9392oveq1d 6542 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9465, 82, 933eqtrd 2648 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9564, 94oveq12d 6545 . . 3 (𝜑 → (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
9628prodeq1d 14439 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
97 nfcv 2751 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(𝐵𝐾)))
9861, 45eqeltrrd 2689 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
9946, 74oveq12d 6545 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝐾)[,)(𝐵𝐾)))
10099fveq2d 6092 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
101 volicore 39265 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
10250, 78, 101syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
103102recnd 9925 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℂ)
10430, 97, 33, 16, 34, 98, 100, 103fprodsplitsn 14508 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
10596, 104eqtrd 2644 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
1065, 6, 3, 7, 16hsphoival 39263 . . . . . . . . . 10 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
10734iffalsed 4047 . . . . . . . . . 10 (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
108106, 107eqtrd 2644 . . . . . . . . 9 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
109108oveq2d 6543 . . . . . . . 8 (𝜑 → ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)) = ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
110109fveq2d 6092 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))))
11111, 6, 3, 4, 16hoidifhspval3 39303 . . . . . . . . . 10 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)))
112 eqid 2610 . . . . . . . . . . . 12 𝐾 = 𝐾
113112iftruei 4043 . . . . . . . . . . 11 if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)
114113a1i 11 . . . . . . . . . 10 (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
115111, 114eqtrd 2644 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
116115oveq1d 6542 . . . . . . . 8 (𝜑 → ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)) = (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))
117116fveq2d 6092 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) = (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))))
118110, 117oveq12d 6545 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
119 iftrue 4042 . . . . . . . . . . . 12 ((𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = (𝐵𝐾))
120119oveq2d 6543 . . . . . . . . . . 11 ((𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)(𝐵𝐾)))
121120fveq2d 6092 . . . . . . . . . 10 ((𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
122121oveq1d 6542 . . . . . . . . 9 ((𝐵𝐾) ≤ 𝑌 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
123122adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
124 iftrue 4042 . . . . . . . . . . . . . . 15 (𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = (𝐴𝐾))
125124oveq1d 6542 . . . . . . . . . . . . . 14 (𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
126125adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
12778ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ)
1286ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
12950ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
130 simplr 788 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ 𝑌)
131 simpr 476 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
132127, 128, 129, 130, 131letrd 10046 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ (𝐴𝐾))
133129rexrd 9946 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
134127rexrd 9946 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ*)
135 ico0 12051 . . . . . . . . . . . . . . 15 (((𝐴𝐾) ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
136133, 134, 135syl2anc 691 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
137132, 136mpbird 246 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)(𝐵𝐾)) = ∅)
138126, 137eqtrd 2644 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
139 iffalse 4045 . . . . . . . . . . . . . . 15 𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = 𝑌)
140139oveq1d 6542 . . . . . . . . . . . . . 14 𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
141140adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
142 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ≤ 𝑌)
1436rexrd 9946 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ ℝ*)
144143adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ*)
14578rexrd 9946 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐾) ∈ ℝ*)
146145adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ*)
147 ico0 12051 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
148144, 146, 147syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
149142, 148mpbird 246 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝑌[,)(𝐵𝐾)) = ∅)
150149adantr 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝑌[,)(𝐵𝐾)) = ∅)
151141, 150eqtrd 2644 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
152138, 151pm2.61dan 828 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
153152fveq2d 6092 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘∅))
154 vol0 38645 . . . . . . . . . . 11 (vol‘∅) = 0
155154a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘∅) = 0)
156153, 155eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = 0)
157156oveq2d 6543 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0))
158103addid1d 10088 . . . . . . . . 9 (𝜑 → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
159158adantr 480 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
160123, 157, 1593eqtrd 2648 . . . . . . 7 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
161 iffalse 4045 . . . . . . . . . . . 12 (¬ (𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = 𝑌)
162161oveq2d 6543 . . . . . . . . . . 11 (¬ (𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)𝑌))
163162fveq2d 6092 . . . . . . . . . 10 (¬ (𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
164163adantl 481 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
165164oveq1d 6542 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
166 simpl 472 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝜑)
167 simpr 476 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ¬ (𝐵𝐾) ≤ 𝑌)
168166, 6syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
169166, 78syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ)
170168, 169ltnled 10036 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝑌 < (𝐵𝐾) ↔ ¬ (𝐵𝐾) ≤ 𝑌))
171167, 170mpbird 246 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 < (𝐵𝐾))
172125fveq2d 6092 . . . . . . . . . . . . 13 (𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
173172oveq2d 6543 . . . . . . . . . . . 12 (𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
174173adantl 481 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
175 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
17650rexrd 9946 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐾) ∈ ℝ*)
177176adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
178143adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ*)
179 ico0 12051 . . . . . . . . . . . . . . . . 17 (((𝐴𝐾) ∈ ℝ*𝑌 ∈ ℝ*) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
180177, 178, 179syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
181175, 180mpbird 246 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)𝑌) = ∅)
182181fveq2d 6092 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = (vol‘∅))
183154a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘∅) = 0)
184182, 183eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = 0)
185184oveq1d 6542 . . . . . . . . . . . 12 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
186185adantlr 747 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
187103addid2d 10089 . . . . . . . . . . . 12 (𝜑 → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
188187ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
189174, 186, 1883eqtrd 2648 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
190140fveq2d 6092 . . . . . . . . . . . . 13 𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘(𝑌[,)(𝐵𝐾))))
191190oveq2d 6543 . . . . . . . . . . . 12 𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
192191adantl 481 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
193 simpl 472 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝜑𝑌 < (𝐵𝐾)))
194 simpr 476 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ¬ 𝑌 ≤ (𝐴𝐾))
19550adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
1966adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
197195, 196ltnled 10036 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴𝐾)))
198194, 197mpbird 246 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
199198adantlr 747 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
20050adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
2016adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
202 volico 38670 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
203200, 201, 202syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
204 iftrue 4042 . . . . . . . . . . . . . . . 16 ((𝐴𝐾) < 𝑌 → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
205204adantl 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
206203, 205eqtrd 2644 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
207206adantlr 747 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
2086adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → 𝑌 ∈ ℝ)
20978adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → (𝐵𝐾) ∈ ℝ)
210 volico 38670 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
211208, 209, 210syl2anc 691 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
212 iftrue 4042 . . . . . . . . . . . . . . . 16 (𝑌 < (𝐵𝐾) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
213212adantl 481 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
214211, 213eqtrd 2644 . . . . . . . . . . . . . 14 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
215214adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
216207, 215oveq12d 6545 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
217193, 199, 216syl2anc 691 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
218200adantlr 747 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
219208adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
220209adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐵𝐾) ∈ ℝ)
221 simpr 476 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < 𝑌)
222 simplr 788 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 < (𝐵𝐾))
223218, 219, 220, 221, 222lttrd 10050 . . . . . . . . . . . . . . 15 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < (𝐵𝐾))
224223iftrued 4044 . . . . . . . . . . . . . 14 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0) = ((𝐵𝐾) − (𝐴𝐾)))
225224eqcomd 2616 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝐵𝐾) − (𝐴𝐾)) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
2266, 50resubcld 10310 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℝ)
227226recnd 9925 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℂ)
22878, 6resubcld 10310 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℝ)
229228recnd 9925 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℂ)
230227, 229addcomd 10090 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))))
23178recnd 9925 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐾) ∈ ℂ)
2326recnd 9925 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
23350recnd 9925 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐾) ∈ ℂ)
234231, 232, 233npncand 10268 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))) = ((𝐵𝐾) − (𝐴𝐾)))
235230, 234eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
236235ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
237 volico 38670 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
238218, 220, 237syl2anc 691 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
239225, 236, 2383eqtr4d 2654 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
240193, 199, 239syl2anc 691 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
241192, 217, 2403eqtrd 2648 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
242189, 241pm2.61dan 828 . . . . . . . . 9 ((𝜑𝑌 < (𝐵𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
243166, 171, 242syl2anc 691 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
244165, 243eqtrd 2644 . . . . . . 7 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
245160, 244pm2.61dan 828 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
246118, 245eqtr2d 2645 . . . . 5 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
247246oveq2d 6543 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
24833, 98fprodcl 14470 . . . . 5 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
249248, 54, 81adddid 9921 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
250105, 247, 2493eqtrrd 2649 . . 3 (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
25121, 95, 2503eqtrd 2648 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
2522, 3, 18, 4, 7hoidmvn0val 39268 . . 3 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
253252eqcomd 2616 . 2 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (𝐴(𝐿𝑋)𝐵))
25415, 251, 2533eqtrrd 2649 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wa 383   = wceq 1475  wcel 1977  wne 2780  cdif 3537  cun 3538  wss 3540  c0 3874  ifcif 4036  {csn 4125   class class class wbr 4578  cmpt 4638  wf 5786  cfv 5790  (class class class)co 6527  cmpt2 6529  𝑚 cmap 7722  Fincfn 7819  cc 9791  cr 9792  0cc0 9793   + caddc 9796   · cmul 9798  +∞cpnf 9928  *cxr 9930   < clt 9931  cle 9932  cmin 10118   +𝑒 cxad 11779  [,)cico 12007  cprod 14423  volcvol 22984
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-fi 8178  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-n0 11143  df-z 11214  df-uz 11523  df-q 11624  df-rp 11668  df-xneg 11781  df-xadd 11782  df-xmul 11783  df-ioo 12009  df-ico 12011  df-icc 12012  df-fz 12156  df-fzo 12293  df-fl 12413  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-rlim 14017  df-sum 14214  df-prod 14424  df-rest 15855  df-topgen 15876  df-psmet 19508  df-xmet 19509  df-met 19510  df-bl 19511  df-mopn 19512  df-top 20469  df-bases 20470  df-topon 20471  df-cmp 20948  df-ovol 22985  df-vol 22986
This theorem is referenced by:  hspmbllem2  39311
  Copyright terms: Public domain W3C validator