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 41480
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 12484 . . . 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 41430 . . . . 5 (𝜑 → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
92, 3, 4, 8hoidmvcl 41436 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ (0[,)+∞))
101, 9sseldi 3759 . . 3 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑𝑚 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
1211, 6, 3, 4hoidifhspf 41472 . . . . 5 (𝜑 → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
132, 3, 12, 7hoidmvcl 41436 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ (0[,)+∞))
141, 13sseldi 3759 . . 3 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ ℝ)
1510, 14rexaddd 12267 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
16 hspmbllem1.k . . . . . 6 (𝜑𝐾𝑋)
1716ne0d 4086 . . . . 5 (𝜑𝑋 ≠ ∅)
182, 3, 17, 4, 8hoidmvn0val 41438 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
192, 3, 17, 12, 7hoidmvn0val 41438 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
2018, 19oveq12d 6860 . . 3 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))))
21 uncom 3919 . . . . . . . . 9 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
2221a1i 11 . . . . . . . 8 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
2316snssd 4494 . . . . . . . . 9 (𝜑 → {𝐾} ⊆ 𝑋)
24 undif 4209 . . . . . . . . 9 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2523, 24sylib 209 . . . . . . . 8 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2622, 25eqtrd 2799 . . . . . . 7 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
2726eqcomd 2771 . . . . . 6 (𝜑𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
2827prodeq1d 14934 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
29 nfv 2009 . . . . . 6 𝑘𝜑
30 nfcv 2907 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
31 difssd 3900 . . . . . . 7 (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
323, 31ssfid 8390 . . . . . 6 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33 neldifsnd 4478 . . . . . 6 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
344adantr 472 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
3531sselda 3761 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘𝑋)
3634, 35ffvelrnd 6550 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴𝑘) ∈ ℝ)
376adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
383adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
397adantr 472 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
405, 37, 38, 39hsphoif 41430 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
4140, 35ffvelrnd 6550 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42 volicore 41435 . . . . . . . 8 (((𝐴𝑘) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4336, 41, 42syl2anc 579 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4443recnd 10322 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45 fveq2 6375 . . . . . . . 8 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
46 fveq2 6375 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑇𝑌)‘𝐵)‘𝑘) = (((𝑇𝑌)‘𝐵)‘𝐾))
4745, 46oveq12d 6860 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
4847fveq2d 6379 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))))
494, 16ffvelrnd 6550 . . . . . . . 8 (𝜑 → (𝐴𝐾) ∈ ℝ)
508, 16ffvelrnd 6550 . . . . . . . 8 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51 volicore 41435 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5249, 50, 51syl2anc 579 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5352recnd 10322 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
5429, 30, 32, 16, 33, 44, 48, 53fprodsplitsn 15002 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
555, 37, 38, 39, 35hsphoival 41433 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)))
56 iftrue 4249 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5756adantl 473 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5855, 57eqtrd 2799 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = (𝐵𝑘))
5958oveq2d 6858 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
6059fveq2d 6379 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6160prodeq2dv 14936 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6261oveq1d 6857 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6328, 54, 623eqtrd 2803 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6427prodeq1d 14934 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
65 nfcv 2907 . . . . . 6 𝑘(vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
6612adantr 472 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
6766, 35ffvelrnd 6550 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ)
6858, 41eqeltrrd 2845 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵𝑘) ∈ ℝ)
69 volicore 41435 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7067, 68, 69syl2anc 579 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7170recnd 10322 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℂ)
72 fveq2 6375 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑆𝑌)‘𝐴)‘𝑘) = (((𝑆𝑌)‘𝐴)‘𝐾))
73 fveq2 6375 . . . . . . . 8 (𝑘 = 𝐾 → (𝐵𝑘) = (𝐵𝐾))
7472, 73oveq12d 6860 . . . . . . 7 (𝑘 = 𝐾 → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
7574fveq2d 6379 . . . . . 6 (𝑘 = 𝐾 → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))
7612, 16ffvelrnd 6550 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ)
777, 16ffvelrnd 6550 . . . . . . . 8 (𝜑 → (𝐵𝐾) ∈ ℝ)
78 volicore 41435 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
7976, 77, 78syl2anc 579 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8079recnd 10322 . . . . . 6 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℂ)
8129, 65, 32, 16, 33, 71, 75, 80fprodsplitsn 15002 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
8211, 37, 38, 34, 35hoidifhspval3 41473 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)))
83 eldifsni 4476 . . . . . . . . . . . 12 (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘𝐾)
84 neneq 2943 . . . . . . . . . . . 12 (𝑘𝐾 → ¬ 𝑘 = 𝐾)
8583, 84syl 17 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
8685iffalsed 4254 . . . . . . . . . 10 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8786adantl 473 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8882, 87eqtrd 2799 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = (𝐴𝑘))
8988fvoveq1d 6864 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9089prodeq2dv 14936 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9190oveq1d 6857 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9264, 81, 913eqtrd 2803 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9363, 92oveq12d 6860 . . 3 (𝜑 → (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
9427prodeq1d 14934 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
95 nfcv 2907 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(𝐵𝐾)))
9660, 44eqeltrrd 2845 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
9745, 73oveq12d 6860 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝐾)[,)(𝐵𝐾)))
9897fveq2d 6379 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
99 volicore 41435 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
10049, 77, 99syl2anc 579 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
101100recnd 10322 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℂ)
10229, 95, 32, 16, 33, 96, 98, 101fprodsplitsn 15002 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
10394, 102eqtrd 2799 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
1045, 6, 3, 7, 16hsphoival 41433 . . . . . . . . . 10 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
10533iffalsed 4254 . . . . . . . . . 10 (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
106104, 105eqtrd 2799 . . . . . . . . 9 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
107106oveq2d 6858 . . . . . . . 8 (𝜑 → ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)) = ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
108107fveq2d 6379 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))))
10911, 6, 3, 4, 16hoidifhspval3 41473 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)))
110 eqid 2765 . . . . . . . . . . 11 𝐾 = 𝐾
111110iftruei 4250 . . . . . . . . . 10 if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)
112111a1i 11 . . . . . . . . 9 (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
113109, 112eqtrd 2799 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
114113fvoveq1d 6864 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) = (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))))
115108, 114oveq12d 6860 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
116 iftrue 4249 . . . . . . . . . . . 12 ((𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = (𝐵𝐾))
117116oveq2d 6858 . . . . . . . . . . 11 ((𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)(𝐵𝐾)))
118117fveq2d 6379 . . . . . . . . . 10 ((𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
119118oveq1d 6857 . . . . . . . . 9 ((𝐵𝐾) ≤ 𝑌 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
120119adantl 473 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
121 iftrue 4249 . . . . . . . . . . . . . . 15 (𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = (𝐴𝐾))
122121oveq1d 6857 . . . . . . . . . . . . . 14 (𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
123122adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
12477ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ)
1256ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
12649ad2antrr 717 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
127 simplr 785 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ 𝑌)
128 simpr 477 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
129124, 125, 126, 127, 128letrd 10448 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ (𝐴𝐾))
130126rexrd 10343 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
131124rexrd 10343 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ*)
132 ico0 12423 . . . . . . . . . . . . . . 15 (((𝐴𝐾) ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
133130, 131, 132syl2anc 579 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
134129, 133mpbird 248 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)(𝐵𝐾)) = ∅)
135123, 134eqtrd 2799 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
136 iffalse 4252 . . . . . . . . . . . . . . 15 𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = 𝑌)
137136oveq1d 6857 . . . . . . . . . . . . . 14 𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
138137adantl 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
139 simpr 477 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ≤ 𝑌)
1406rexrd 10343 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ ℝ*)
141140adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ*)
14277rexrd 10343 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐾) ∈ ℝ*)
143142adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ*)
144 ico0 12423 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
145141, 143, 144syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
146139, 145mpbird 248 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝑌[,)(𝐵𝐾)) = ∅)
147146adantr 472 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝑌[,)(𝐵𝐾)) = ∅)
148138, 147eqtrd 2799 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
149135, 148pm2.61dan 847 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
150149fveq2d 6379 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘∅))
151 vol0 40812 . . . . . . . . . . 11 (vol‘∅) = 0
152151a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153150, 152eqtrd 2799 . . . . . . . . 9 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = 0)
154153oveq2d 6858 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0))
155101addid1d 10490 . . . . . . . . 9 (𝜑 → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
156155adantr 472 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
157120, 154, 1563eqtrd 2803 . . . . . . 7 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
158 iffalse 4252 . . . . . . . . . . . 12 (¬ (𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = 𝑌)
159158oveq2d 6858 . . . . . . . . . . 11 (¬ (𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)𝑌))
160159fveq2d 6379 . . . . . . . . . 10 (¬ (𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
161160adantl 473 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
162161oveq1d 6857 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
163 simpl 474 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝜑)
164 simpr 477 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ¬ (𝐵𝐾) ≤ 𝑌)
165163, 6syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
166163, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ)
167165, 166ltnled 10438 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝑌 < (𝐵𝐾) ↔ ¬ (𝐵𝐾) ≤ 𝑌))
168164, 167mpbird 248 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 < (𝐵𝐾))
169121fvoveq1d 6864 . . . . . . . . . . . . 13 (𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
170169oveq2d 6858 . . . . . . . . . . . 12 (𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
171170adantl 473 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
172 simpr 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
17349rexrd 10343 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐾) ∈ ℝ*)
174173adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
175140adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ*)
176 ico0 12423 . . . . . . . . . . . . . . . . 17 (((𝐴𝐾) ∈ ℝ*𝑌 ∈ ℝ*) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
177174, 175, 176syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
178172, 177mpbird 248 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)𝑌) = ∅)
179178fveq2d 6379 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = (vol‘∅))
180151a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘∅) = 0)
181179, 180eqtrd 2799 . . . . . . . . . . . . 13 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = 0)
182181oveq1d 6857 . . . . . . . . . . . 12 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
183182adantlr 706 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
184101addid2d 10491 . . . . . . . . . . . 12 (𝜑 → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
185184ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
186171, 183, 1853eqtrd 2803 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
187136fvoveq1d 6864 . . . . . . . . . . . . 13 𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘(𝑌[,)(𝐵𝐾))))
188187oveq2d 6858 . . . . . . . . . . . 12 𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
189188adantl 473 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
190 simpl 474 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝜑𝑌 < (𝐵𝐾)))
191 simpr 477 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ¬ 𝑌 ≤ (𝐴𝐾))
19249adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
1936adantr 472 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
194192, 193ltnled 10438 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴𝐾)))
195191, 194mpbird 248 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
196195adantlr 706 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
19749adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
1986adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199 volico 40837 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
200197, 198, 199syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
201 iftrue 4249 . . . . . . . . . . . . . . . 16 ((𝐴𝐾) < 𝑌 → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
202201adantl 473 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
203200, 202eqtrd 2799 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
204203adantlr 706 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
2056adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → 𝑌 ∈ ℝ)
20677adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → (𝐵𝐾) ∈ ℝ)
207 volico 40837 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
208205, 206, 207syl2anc 579 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
209 iftrue 4249 . . . . . . . . . . . . . . . 16 (𝑌 < (𝐵𝐾) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
210209adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
211208, 210eqtrd 2799 . . . . . . . . . . . . . 14 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
212211adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
213204, 212oveq12d 6860 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
214190, 196, 213syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
215197adantlr 706 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
216205adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
217206adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐵𝐾) ∈ ℝ)
218 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < 𝑌)
219 simplr 785 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 < (𝐵𝐾))
220215, 216, 217, 218, 219lttrd 10452 . . . . . . . . . . . . . . 15 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < (𝐵𝐾))
221220iftrued 4251 . . . . . . . . . . . . . 14 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0) = ((𝐵𝐾) − (𝐴𝐾)))
222221eqcomd 2771 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝐵𝐾) − (𝐴𝐾)) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
2236, 49resubcld 10712 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℝ)
224223recnd 10322 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℂ)
22577, 6resubcld 10712 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℝ)
226225recnd 10322 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℂ)
227224, 226addcomd 10492 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))))
22877recnd 10322 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐾) ∈ ℂ)
2296recnd 10322 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
23049recnd 10322 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐾) ∈ ℂ)
231228, 229, 230npncand 10670 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))) = ((𝐵𝐾) − (𝐴𝐾)))
232227, 231eqtrd 2799 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
233232ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
234 volico 40837 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
235215, 217, 234syl2anc 579 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
236222, 233, 2353eqtr4d 2809 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
237190, 196, 236syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
238189, 214, 2373eqtrd 2803 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
239186, 238pm2.61dan 847 . . . . . . . . 9 ((𝜑𝑌 < (𝐵𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
240163, 168, 239syl2anc 579 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
241162, 240eqtrd 2799 . . . . . . 7 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
242157, 241pm2.61dan 847 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
243115, 242eqtr2d 2800 . . . . 5 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
244243oveq2d 6858 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
24532, 96fprodcl 14965 . . . . 5 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
246245, 53, 80adddid 10318 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
247103, 244, 2463eqtrrd 2804 . . 3 (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24820, 93, 2473eqtrd 2803 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
2492, 3, 17, 4, 7hoidmvn0val 41438 . . 3 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
250249eqcomd 2771 . 2 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (𝐴(𝐿𝑋)𝐵))
25115, 248, 2503eqtrrd 2804 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wne 2937  cdif 3729  cun 3730  wss 3732  c0 4079  ifcif 4243  {csn 4334   class class class wbr 4809  cmpt 4888  wf 6064  cfv 6068  (class class class)co 6842  cmpt2 6844  𝑚 cmap 8060  Fincfn 8160  cc 10187  cr 10188  0cc0 10189   + caddc 10192   · cmul 10194  +∞cpnf 10325  *cxr 10327   < clt 10328  cle 10329  cmin 10520   +𝑒 cxad 12144  [,)cico 12379  cprod 14918  volcvol 23521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-inf2 8753  ax-cnex 10245  ax-resscn 10246  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-mulcom 10253  ax-addass 10254  ax-mulass 10255  ax-distr 10256  ax-i2m1 10257  ax-1ne0 10258  ax-1rid 10259  ax-rnegex 10260  ax-rrecex 10261  ax-cnre 10262  ax-pre-lttri 10263  ax-pre-lttrn 10264  ax-pre-ltadd 10265  ax-pre-mulgt0 10266  ax-pre-sup 10267
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-isom 6077  df-riota 6803  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-of 7095  df-om 7264  df-1st 7366  df-2nd 7367  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-2o 7765  df-oadd 7768  df-er 7947  df-map 8062  df-pm 8063  df-en 8161  df-dom 8162  df-sdom 8163  df-fin 8164  df-fi 8524  df-sup 8555  df-inf 8556  df-oi 8622  df-card 9016  df-cda 9243  df-pnf 10330  df-mnf 10331  df-xr 10332  df-ltxr 10333  df-le 10334  df-sub 10522  df-neg 10523  df-div 10939  df-nn 11275  df-2 11335  df-3 11336  df-n0 11539  df-z 11625  df-uz 11887  df-q 11990  df-rp 12029  df-xneg 12146  df-xadd 12147  df-xmul 12148  df-ioo 12381  df-ico 12383  df-icc 12384  df-fz 12534  df-fzo 12674  df-fl 12801  df-seq 13009  df-exp 13068  df-hash 13322  df-cj 14124  df-re 14125  df-im 14126  df-sqrt 14260  df-abs 14261  df-clim 14504  df-rlim 14505  df-sum 14702  df-prod 14919  df-rest 16349  df-topgen 16370  df-psmet 20011  df-xmet 20012  df-met 20013  df-bl 20014  df-mopn 20015  df-top 20978  df-topon 20995  df-bases 21030  df-cmp 21470  df-ovol 23522  df-vol 23523
This theorem is referenced by:  hspmbllem2  41481
  Copyright terms: Public domain W3C validator