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

Theorem hspmbllem1 39516
 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 12151 . . . 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 39466 . . . . 5 (𝜑 → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
92, 3, 4, 8hoidmvcl 39472 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ (0[,)+∞))
101, 9sseldi 3566 . . 3 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
1211, 6, 3, 4hoidifhspf 39508 . . . . 5 (𝜑 → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
132, 3, 12, 7hoidmvcl 39472 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ (0[,)+∞))
141, 13sseldi 3566 . . 3 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ ℝ)
1510, 14rexaddd 11939 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
16 hspmbllem1.k . . . . . 6 (𝜑𝐾𝑋)
17 ne0i 3880 . . . . . 6 (𝐾𝑋𝑋 ≠ ∅)
1816, 17syl 17 . . . . 5 (𝜑𝑋 ≠ ∅)
192, 3, 18, 4, 8hoidmvn0val 39474 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
202, 3, 18, 12, 7hoidmvn0val 39474 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
2119, 20oveq12d 6567 . . 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 14490 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
30 nfv 1830 . . . . . 6 𝑘𝜑
31 nfcv 2751 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
32 difssd 3700 . . . . . . 7 (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
333, 32ssfid 8068 . . . . . 6 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
34 neldifsnd 4263 . . . . . 6 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
354adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
3632sselda 3568 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘𝑋)
3735, 36ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴𝑘) ∈ ℝ)
386adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
393adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
407adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
415, 38, 39, 40hsphoif 39466 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
4241, 36ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ)
43 volicore 39471 . . . . . . . 8 (((𝐴𝑘) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4437, 42, 43syl2anc 691 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4544recnd 9947 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
46 fveq2 6103 . . . . . . . 8 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
47 fveq2 6103 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑇𝑌)‘𝐵)‘𝑘) = (((𝑇𝑌)‘𝐵)‘𝐾))
4846, 47oveq12d 6567 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
4948fveq2d 6107 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))))
504, 16ffvelrnd 6268 . . . . . . . 8 (𝜑 → (𝐴𝐾) ∈ ℝ)
518, 16ffvelrnd 6268 . . . . . . . 8 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ)
52 volicore 39471 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5350, 51, 52syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5453recnd 9947 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
5530, 31, 33, 16, 34, 45, 49, 54fprodsplitsn 14559 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
565, 38, 39, 40, 36hsphoival 39469 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)))
57 iftrue 4042 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5857adantl 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5956, 58eqtrd 2644 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = (𝐵𝑘))
6059oveq2d 6565 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
6160fveq2d 6107 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6261prodeq2dv 14492 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6362oveq1d 6564 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6429, 55, 633eqtrd 2648 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6528prodeq1d 14490 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
66 nfcv 2751 . . . . . 6 𝑘(vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
6712adantr 480 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
6867, 36ffvelrnd 6268 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ)
6959, 42eqeltrrd 2689 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵𝑘) ∈ ℝ)
70 volicore 39471 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7168, 69, 70syl2anc 691 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7271recnd 9947 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℂ)
73 fveq2 6103 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑆𝑌)‘𝐴)‘𝑘) = (((𝑆𝑌)‘𝐴)‘𝐾))
74 fveq2 6103 . . . . . . . 8 (𝑘 = 𝐾 → (𝐵𝑘) = (𝐵𝐾))
7573, 74oveq12d 6567 . . . . . . 7 (𝑘 = 𝐾 → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
7675fveq2d 6107 . . . . . 6 (𝑘 = 𝐾 → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))
7712, 16ffvelrnd 6268 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ)
787, 16ffvelrnd 6268 . . . . . . . 8 (𝜑 → (𝐵𝐾) ∈ ℝ)
79 volicore 39471 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8077, 78, 79syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8180recnd 9947 . . . . . 6 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℂ)
8230, 66, 33, 16, 34, 72, 76, 81fprodsplitsn 14559 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
8311, 38, 39, 35, 36hoidifhspval3 39509 . . . . . . . . . 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 6564 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
9190fveq2d 6107 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9291prodeq2dv 14492 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9392oveq1d 6564 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9465, 82, 933eqtrd 2648 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9564, 94oveq12d 6567 . . 3 (𝜑 → (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
9628prodeq1d 14490 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
97 nfcv 2751 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(𝐵𝐾)))
9861, 45eqeltrrd 2689 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
9946, 74oveq12d 6567 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝐾)[,)(𝐵𝐾)))
10099fveq2d 6107 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
101 volicore 39471 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
10250, 78, 101syl2anc 691 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
103102recnd 9947 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℂ)
10430, 97, 33, 16, 34, 98, 100, 103fprodsplitsn 14559 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
10596, 104eqtrd 2644 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
1065, 6, 3, 7, 16hsphoival 39469 . . . . . . . . . 10 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
10734iffalsed 4047 . . . . . . . . . 10 (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
108106, 107eqtrd 2644 . . . . . . . . 9 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
109108oveq2d 6565 . . . . . . . 8 (𝜑 → ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)) = ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
110109fveq2d 6107 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))))
11111, 6, 3, 4, 16hoidifhspval3 39509 . . . . . . . . . 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 6564 . . . . . . . 8 (𝜑 → ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)) = (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))
117116fveq2d 6107 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) = (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))))
118110, 117oveq12d 6567 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
119 iftrue 4042 . . . . . . . . . . . 12 ((𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = (𝐵𝐾))
120119oveq2d 6565 . . . . . . . . . . 11 ((𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)(𝐵𝐾)))
121120fveq2d 6107 . . . . . . . . . 10 ((𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
122121oveq1d 6564 . . . . . . . . 9 ((𝐵𝐾) ≤ 𝑌 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
123122adantl 481 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
124 iftrue 4042 . . . . . . . . . . . . . . 15 (𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = (𝐴𝐾))
125124oveq1d 6564 . . . . . . . . . . . . . 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 10073 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ (𝐴𝐾))
133129rexrd 9968 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
134127rexrd 9968 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ*)
135 ico0 12092 . . . . . . . . . . . . . . 15 (((𝐴𝐾) ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
136133, 134, 135syl2anc 691 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
137132, 136mpbird 246 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)(𝐵𝐾)) = ∅)
138126, 137eqtrd 2644 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
139 iffalse 4045 . . . . . . . . . . . . . . 15 𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = 𝑌)
140139oveq1d 6564 . . . . . . . . . . . . . 14 𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
141140adantl 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
142 simpr 476 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ≤ 𝑌)
1436rexrd 9968 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ ℝ*)
144143adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ*)
14578rexrd 9968 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐾) ∈ ℝ*)
146145adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ*)
147 ico0 12092 . . . . . . . . . . . . . . . 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 6107 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘∅))
154 vol0 38851 . . . . . . . . . . 11 (vol‘∅) = 0
155154a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘∅) = 0)
156153, 155eqtrd 2644 . . . . . . . . 9 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = 0)
157156oveq2d 6565 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0))
158103addid1d 10115 . . . . . . . . 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 6565 . . . . . . . . . . 11 (¬ (𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)𝑌))
163162fveq2d 6107 . . . . . . . . . 10 (¬ (𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
164163adantl 481 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
165164oveq1d 6564 . . . . . . . 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 10063 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝑌 < (𝐵𝐾) ↔ ¬ (𝐵𝐾) ≤ 𝑌))
171167, 170mpbird 246 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 < (𝐵𝐾))
172125fveq2d 6107 . . . . . . . . . . . . 13 (𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
173172oveq2d 6565 . . . . . . . . . . . 12 (𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
174173adantl 481 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
175 simpr 476 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
17650rexrd 9968 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐾) ∈ ℝ*)
177176adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
178143adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ*)
179 ico0 12092 . . . . . . . . . . . . . . . . 17 (((𝐴𝐾) ∈ ℝ*𝑌 ∈ ℝ*) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
180177, 178, 179syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
181175, 180mpbird 246 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)𝑌) = ∅)
182181fveq2d 6107 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = (vol‘∅))
183154a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘∅) = 0)
184182, 183eqtrd 2644 . . . . . . . . . . . . 13 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = 0)
185184oveq1d 6564 . . . . . . . . . . . 12 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
186185adantlr 747 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
187103addid2d 10116 . . . . . . . . . . . 12 (𝜑 → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
188187ad2antrr 758 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
189174, 186, 1883eqtrd 2648 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
190140fveq2d 6107 . . . . . . . . . . . . 13 𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘(𝑌[,)(𝐵𝐾))))
191190oveq2d 6565 . . . . . . . . . . . 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 10063 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴𝐾)))
198194, 197mpbird 246 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
199198adantlr 747 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
20050adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
2016adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
202 volico 38876 . . . . . . . . . . . . . . . 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 38876 . . . . . . . . . . . . . . . 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 6567 . . . . . . . . . . . 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 10077 . . . . . . . . . . . . . . 15 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < (𝐵𝐾))
224223iftrued 4044 . . . . . . . . . . . . . 14 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0) = ((𝐵𝐾) − (𝐴𝐾)))
225224eqcomd 2616 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝐵𝐾) − (𝐴𝐾)) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
2266, 50resubcld 10337 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℝ)
227226recnd 9947 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℂ)
22878, 6resubcld 10337 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℝ)
229228recnd 9947 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℂ)
230227, 229addcomd 10117 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))))
23178recnd 9947 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐾) ∈ ℂ)
2326recnd 9947 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
23350recnd 9947 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐾) ∈ ℂ)
234231, 232, 233npncand 10295 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))) = ((𝐵𝐾) − (𝐴𝐾)))
235230, 234eqtrd 2644 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
236235ad2antrr 758 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
237 volico 38876 . . . . . . . . . . . . . 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 6565 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
24833, 98fprodcl 14521 . . . . 5 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
249248, 54, 81adddid 9943 . . . 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 39474 . . 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 4583   ↦ cmpt 4643  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551   ↑𝑚 cmap 7744  Fincfn 7841  ℂcc 9813  ℝcr 9814  0cc0 9815   + caddc 9818   · cmul 9820  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   − cmin 10145   +𝑒 cxad 11820  [,)cico 12048  ∏cprod 14474  volcvol 23039 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 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 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 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-of 6795  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-oi 8298  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-rp 11709  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ioo 12050  df-ico 12052  df-icc 12053  df-fz 12198  df-fzo 12335  df-fl 12455  df-seq 12664  df-exp 12723  df-hash 12980  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068  df-sum 14265  df-prod 14475  df-rest 15906  df-topgen 15927  df-psmet 19559  df-xmet 19560  df-met 19561  df-bl 19562  df-mopn 19563  df-top 20521  df-bases 20522  df-topon 20523  df-cmp 21000  df-ovol 23040  df-vol 23041 This theorem is referenced by:  hspmbllem2  39517
 Copyright terms: Public domain W3C validator