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 42785
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 12832 . . . 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 42735 . . . . 5 (𝜑 → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
92, 3, 4, 8hoidmvcl 42741 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ (0[,)+∞))
101, 9sseldi 3962 . . 3 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (𝑥 ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (𝑋 ↦ if( = 𝐾, if(𝑥 ≤ (𝑐), (𝑐), 𝑥), (𝑐)))))
1211, 6, 3, 4hoidifhspf 42777 . . . . 5 (𝜑 → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
132, 3, 12, 7hoidmvcl 42741 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ (0[,)+∞))
141, 13sseldi 3962 . . 3 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) ∈ ℝ)
1510, 14rexaddd 12615 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
16 hspmbllem1.k . . . . . 6 (𝜑𝐾𝑋)
1716ne0d 4298 . . . . 5 (𝜑𝑋 ≠ ∅)
182, 3, 17, 4, 8hoidmvn0val 42743 . . . 4 (𝜑 → (𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
192, 3, 17, 12, 7hoidmvn0val 42743 . . . 4 (𝜑 → (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
2018, 19oveq12d 7163 . . 3 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))))
21 uncom 4126 . . . . . . . . 9 ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾}))
2221a1i 11 . . . . . . . 8 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = ({𝐾} ∪ (𝑋 ∖ {𝐾})))
2316snssd 4734 . . . . . . . . 9 (𝜑 → {𝐾} ⊆ 𝑋)
24 undif 4426 . . . . . . . . 9 ({𝐾} ⊆ 𝑋 ↔ ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2523, 24sylib 219 . . . . . . . 8 (𝜑 → ({𝐾} ∪ (𝑋 ∖ {𝐾})) = 𝑋)
2622, 25eqtrd 2853 . . . . . . 7 (𝜑 → ((𝑋 ∖ {𝐾}) ∪ {𝐾}) = 𝑋)
2726eqcomd 2824 . . . . . 6 (𝜑𝑋 = ((𝑋 ∖ {𝐾}) ∪ {𝐾}))
2827prodeq1d 15263 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))))
29 nfv 1906 . . . . . 6 𝑘𝜑
30 nfcv 2974 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
31 difssd 4106 . . . . . . 7 (𝜑 → (𝑋 ∖ {𝐾}) ⊆ 𝑋)
323, 31ssfid 8729 . . . . . 6 (𝜑 → (𝑋 ∖ {𝐾}) ∈ Fin)
33 neldifsnd 4718 . . . . . 6 (𝜑 → ¬ 𝐾 ∈ (𝑋 ∖ {𝐾}))
344adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐴:𝑋⟶ℝ)
3531sselda 3964 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑘𝑋)
3634, 35ffvelrnd 6844 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐴𝑘) ∈ ℝ)
376adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑌 ∈ ℝ)
383adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝑋 ∈ Fin)
397adantr 481 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → 𝐵:𝑋⟶ℝ)
405, 37, 38, 39hsphoif 42735 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑇𝑌)‘𝐵):𝑋⟶ℝ)
4140, 35ffvelrnd 6844 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ)
42 volicore 42740 . . . . . . . 8 (((𝐴𝑘) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝑘) ∈ ℝ) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4336, 41, 42syl2anc 584 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℝ)
4443recnd 10657 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) ∈ ℂ)
45 fveq2 6663 . . . . . . . 8 (𝑘 = 𝐾 → (𝐴𝑘) = (𝐴𝐾))
46 fveq2 6663 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑇𝑌)‘𝐵)‘𝑘) = (((𝑇𝑌)‘𝐵)‘𝐾))
4745, 46oveq12d 7163 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))
4847fveq2d 6667 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))))
494, 16ffvelrnd 6844 . . . . . . . 8 (𝜑 → (𝐴𝐾) ∈ ℝ)
508, 16ffvelrnd 6844 . . . . . . . 8 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ)
51 volicore 42740 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (((𝑇𝑌)‘𝐵)‘𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5249, 50, 51syl2anc 584 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℝ)
5352recnd 10657 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) ∈ ℂ)
5429, 30, 32, 16, 33, 44, 48, 53fprodsplitsn 15331 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
555, 37, 38, 39, 35hsphoival 42738 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)))
56 iftrue 4469 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5756adantl 482 . . . . . . . . . 10 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 ∈ (𝑋 ∖ {𝐾}), (𝐵𝑘), if((𝐵𝑘) ≤ 𝑌, (𝐵𝑘), 𝑌)) = (𝐵𝑘))
5855, 57eqtrd 2853 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑇𝑌)‘𝐵)‘𝑘) = (𝐵𝑘))
5958oveq2d 7161 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘)) = ((𝐴𝑘)[,)(𝐵𝑘)))
6059fveq2d 6667 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6160prodeq2dv 15265 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
6261oveq1d 7160 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6328, 54, 623eqtrd 2857 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))))
6427prodeq1d 15263 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))))
65 nfcv 2974 . . . . . 6 𝑘(vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
6612adantr 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → ((𝑆𝑌)‘𝐴):𝑋⟶ℝ)
6766, 35ffvelrnd 6844 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ)
6858, 41eqeltrrd 2911 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (𝐵𝑘) ∈ ℝ)
69 volicore 42740 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝑘) ∈ ℝ ∧ (𝐵𝑘) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7067, 68, 69syl2anc 584 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℝ)
7170recnd 10657 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) ∈ ℂ)
72 fveq2 6663 . . . . . . . 8 (𝑘 = 𝐾 → (((𝑆𝑌)‘𝐴)‘𝑘) = (((𝑆𝑌)‘𝐴)‘𝐾))
73 fveq2 6663 . . . . . . . 8 (𝑘 = 𝐾 → (𝐵𝑘) = (𝐵𝐾))
7472, 73oveq12d 7163 . . . . . . 7 (𝑘 = 𝐾 → ((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)) = ((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))
7574fveq2d 6667 . . . . . 6 (𝑘 = 𝐾 → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))
7612, 16ffvelrnd 6844 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ)
777, 16ffvelrnd 6844 . . . . . . . 8 (𝜑 → (𝐵𝐾) ∈ ℝ)
78 volicore 42740 . . . . . . . 8 (((((𝑆𝑌)‘𝐴)‘𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
7976, 77, 78syl2anc 584 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℝ)
8079recnd 10657 . . . . . 6 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) ∈ ℂ)
8129, 65, 32, 16, 33, 71, 75, 80fprodsplitsn 15331 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
8211, 37, 38, 34, 35hoidifhspval3 42778 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)))
83 eldifsni 4714 . . . . . . . . . . . 12 (𝑘 ∈ (𝑋 ∖ {𝐾}) → 𝑘𝐾)
84 neneq 3019 . . . . . . . . . . . 12 (𝑘𝐾 → ¬ 𝑘 = 𝐾)
8583, 84syl 17 . . . . . . . . . . 11 (𝑘 ∈ (𝑋 ∖ {𝐾}) → ¬ 𝑘 = 𝐾)
8685iffalsed 4474 . . . . . . . . . 10 (𝑘 ∈ (𝑋 ∖ {𝐾}) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8786adantl 482 . . . . . . . . 9 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → if(𝑘 = 𝐾, if(𝑌 ≤ (𝐴𝑘), (𝐴𝑘), 𝑌), (𝐴𝑘)) = (𝐴𝑘))
8882, 87eqtrd 2853 . . . . . . . 8 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (((𝑆𝑌)‘𝐴)‘𝑘) = (𝐴𝑘))
8988fvoveq1d 7167 . . . . . . 7 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9089prodeq2dv 15265 . . . . . 6 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
9190oveq1d 7160 . . . . 5 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9264, 81, 913eqtrd 2857 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
9363, 92oveq12d 7163 . . 3 (𝜑 → (∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(((𝑇𝑌)‘𝐵)‘𝑘))) + ∏𝑘𝑋 (vol‘((((𝑆𝑌)‘𝐴)‘𝑘)[,)(𝐵𝑘)))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
9427prodeq1d 15263 . . . . 5 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))))
95 nfcv 2974 . . . . . 6 𝑘(vol‘((𝐴𝐾)[,)(𝐵𝐾)))
9660, 44eqeltrrd 2911 . . . . . 6 ((𝜑𝑘 ∈ (𝑋 ∖ {𝐾})) → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
9745, 73oveq12d 7163 . . . . . . 7 (𝑘 = 𝐾 → ((𝐴𝑘)[,)(𝐵𝑘)) = ((𝐴𝐾)[,)(𝐵𝐾)))
9897fveq2d 6667 . . . . . 6 (𝑘 = 𝐾 → (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
99 volicore 42740 . . . . . . . 8 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
10049, 77, 99syl2anc 584 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℝ)
101100recnd 10657 . . . . . 6 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) ∈ ℂ)
10229, 95, 32, 16, 33, 96, 98, 101fprodsplitsn 15331 . . . . 5 (𝜑 → ∏𝑘 ∈ ((𝑋 ∖ {𝐾}) ∪ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
10394, 102eqtrd 2853 . . . 4 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
1045, 6, 3, 7, 16hsphoival 42738 . . . . . . . . . 10 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
10533iffalsed 4474 . . . . . . . . . 10 (𝜑 → if(𝐾 ∈ (𝑋 ∖ {𝐾}), (𝐵𝐾), if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
106104, 105eqtrd 2853 . . . . . . . . 9 (𝜑 → (((𝑇𝑌)‘𝐵)‘𝐾) = if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))
107106oveq2d 7161 . . . . . . . 8 (𝜑 → ((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)) = ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)))
108107fveq2d 6667 . . . . . . 7 (𝜑 → (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) = (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))))
10911, 6, 3, 4, 16hoidifhspval3 42778 . . . . . . . . 9 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)))
110 eqid 2818 . . . . . . . . . . 11 𝐾 = 𝐾
111110iftruei 4470 . . . . . . . . . 10 if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)
112111a1i 11 . . . . . . . . 9 (𝜑 → if(𝐾 = 𝐾, if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌), (𝐴𝐾)) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
113109, 112eqtrd 2853 . . . . . . . 8 (𝜑 → (((𝑆𝑌)‘𝐴)‘𝐾) = if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌))
114113fvoveq1d 7167 . . . . . . 7 (𝜑 → (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))) = (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))))
115108, 114oveq12d 7163 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
116 iftrue 4469 . . . . . . . . . . . 12 ((𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = (𝐵𝐾))
117116oveq2d 7161 . . . . . . . . . . 11 ((𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)(𝐵𝐾)))
118117fveq2d 6667 . . . . . . . . . 10 ((𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
119118oveq1d 7160 . . . . . . . . 9 ((𝐵𝐾) ≤ 𝑌 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
120119adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
121 iftrue 4469 . . . . . . . . . . . . . . 15 (𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = (𝐴𝐾))
122121oveq1d 7160 . . . . . . . . . . . . . 14 (𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
123122adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ((𝐴𝐾)[,)(𝐵𝐾)))
12477ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ)
1256ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
12649ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
127 simplr 765 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ 𝑌)
128 simpr 485 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
129124, 125, 126, 127, 128letrd 10785 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ≤ (𝐴𝐾))
130126rexrd 10679 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
131124rexrd 10679 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (𝐵𝐾) ∈ ℝ*)
132 ico0 12772 . . . . . . . . . . . . . . 15 (((𝐴𝐾) ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
133130, 131, 132syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ (𝐴𝐾)))
134129, 133mpbird 258 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)(𝐵𝐾)) = ∅)
135123, 134eqtrd 2853 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
136 iffalse 4472 . . . . . . . . . . . . . . 15 𝑌 ≤ (𝐴𝐾) → if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌) = 𝑌)
137136oveq1d 7160 . . . . . . . . . . . . . 14 𝑌 ≤ (𝐴𝐾) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
138137adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = (𝑌[,)(𝐵𝐾)))
139 simpr 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ≤ 𝑌)
1406rexrd 10679 . . . . . . . . . . . . . . . . 17 (𝜑𝑌 ∈ ℝ*)
141140adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ*)
14277rexrd 10679 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝐾) ∈ ℝ*)
143142adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ*)
144 ico0 12772 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ* ∧ (𝐵𝐾) ∈ ℝ*) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
145141, 143, 144syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((𝑌[,)(𝐵𝐾)) = ∅ ↔ (𝐵𝐾) ≤ 𝑌))
146139, 145mpbird 258 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (𝑌[,)(𝐵𝐾)) = ∅)
147146adantr 481 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝑌[,)(𝐵𝐾)) = ∅)
148138, 147eqtrd 2853 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
149135, 148pm2.61dan 809 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)) = ∅)
150149fveq2d 6667 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘∅))
151 vol0 42120 . . . . . . . . . . 11 (vol‘∅) = 0
152151a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘∅) = 0)
153150, 152eqtrd 2853 . . . . . . . . 9 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = 0)
154153oveq2d 7161 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0))
155101addid1d 10828 . . . . . . . . 9 (𝜑 → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
156155adantr 481 . . . . . . . 8 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)(𝐵𝐾))) + 0) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
157120, 154, 1563eqtrd 2857 . . . . . . 7 ((𝜑 ∧ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
158 iffalse 4472 . . . . . . . . . . . 12 (¬ (𝐵𝐾) ≤ 𝑌 → if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌) = 𝑌)
159158oveq2d 7161 . . . . . . . . . . 11 (¬ (𝐵𝐾) ≤ 𝑌 → ((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌)) = ((𝐴𝐾)[,)𝑌))
160159fveq2d 6667 . . . . . . . . . 10 (¬ (𝐵𝐾) ≤ 𝑌 → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
161160adantl 482 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) = (vol‘((𝐴𝐾)[,)𝑌)))
162161oveq1d 7160 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))))
163 simpl 483 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝜑)
164 simpr 485 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ¬ (𝐵𝐾) ≤ 𝑌)
165163, 6syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 ∈ ℝ)
166163, 77syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝐵𝐾) ∈ ℝ)
167165, 166ltnled 10775 . . . . . . . . . 10 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → (𝑌 < (𝐵𝐾) ↔ ¬ (𝐵𝐾) ≤ 𝑌))
168164, 167mpbird 258 . . . . . . . . 9 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → 𝑌 < (𝐵𝐾))
169121fvoveq1d 7167 . . . . . . . . . . . . 13 (𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
170169oveq2d 7161 . . . . . . . . . . . 12 (𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
171170adantl 482 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
172 simpr 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ≤ (𝐴𝐾))
17349rexrd 10679 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴𝐾) ∈ ℝ*)
174173adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ*)
175140adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ*)
176 ico0 12772 . . . . . . . . . . . . . . . . 17 (((𝐴𝐾) ∈ ℝ*𝑌 ∈ ℝ*) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
177174, 175, 176syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 ≤ (𝐴𝐾)) → (((𝐴𝐾)[,)𝑌) = ∅ ↔ 𝑌 ≤ (𝐴𝐾)))
178172, 177mpbird 258 . . . . . . . . . . . . . . 15 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾)[,)𝑌) = ∅)
179178fveq2d 6667 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = (vol‘∅))
180151a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘∅) = 0)
181179, 180eqtrd 2853 . . . . . . . . . . . . 13 ((𝜑𝑌 ≤ (𝐴𝐾)) → (vol‘((𝐴𝐾)[,)𝑌)) = 0)
182181oveq1d 7160 . . . . . . . . . . . 12 ((𝜑𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
183182adantlr 711 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))))
184101addid2d 10829 . . . . . . . . . . . 12 (𝜑 → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
185184ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → (0 + (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
186171, 183, 1853eqtrd 2857 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
187136fvoveq1d 7167 . . . . . . . . . . . . 13 𝑌 ≤ (𝐴𝐾) → (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾))) = (vol‘(𝑌[,)(𝐵𝐾))))
188187oveq2d 7161 . . . . . . . . . . . 12 𝑌 ≤ (𝐴𝐾) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
189188adantl 482 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))))
190 simpl 483 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝜑𝑌 < (𝐵𝐾)))
191 simpr 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ¬ 𝑌 ≤ (𝐴𝐾))
19249adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) ∈ ℝ)
1936adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → 𝑌 ∈ ℝ)
194192, 193ltnled 10775 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝐴𝐾) < 𝑌 ↔ ¬ 𝑌 ≤ (𝐴𝐾)))
195191, 194mpbird 258 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
196195adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → (𝐴𝐾) < 𝑌)
19749adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
1986adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
199 volico 42145 . . . . . . . . . . . . . . . 16 (((𝐴𝐾) ∈ ℝ ∧ 𝑌 ∈ ℝ) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
200197, 198, 199syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0))
201 iftrue 4469 . . . . . . . . . . . . . . . 16 ((𝐴𝐾) < 𝑌 → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
202201adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < 𝑌, (𝑌 − (𝐴𝐾)), 0) = (𝑌 − (𝐴𝐾)))
203200, 202eqtrd 2853 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
204203adantlr 711 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)𝑌)) = (𝑌 − (𝐴𝐾)))
2056adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → 𝑌 ∈ ℝ)
20677adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑌 < (𝐵𝐾)) → (𝐵𝐾) ∈ ℝ)
207 volico 42145 . . . . . . . . . . . . . . . 16 ((𝑌 ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
208205, 206, 207syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0))
209 iftrue 4469 . . . . . . . . . . . . . . . 16 (𝑌 < (𝐵𝐾) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
210209adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑌 < (𝐵𝐾)) → if(𝑌 < (𝐵𝐾), ((𝐵𝐾) − 𝑌), 0) = ((𝐵𝐾) − 𝑌))
211208, 210eqtrd 2853 . . . . . . . . . . . . . 14 ((𝜑𝑌 < (𝐵𝐾)) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
212211adantr 481 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘(𝑌[,)(𝐵𝐾))) = ((𝐵𝐾) − 𝑌))
213204, 212oveq12d 7163 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
214190, 196, 213syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(𝑌[,)(𝐵𝐾)))) = ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)))
215197adantlr 711 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) ∈ ℝ)
216205adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 ∈ ℝ)
217206adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐵𝐾) ∈ ℝ)
218 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < 𝑌)
219 simplr 765 . . . . . . . . . . . . . . . 16 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → 𝑌 < (𝐵𝐾))
220215, 216, 217, 218, 219lttrd 10789 . . . . . . . . . . . . . . 15 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (𝐴𝐾) < (𝐵𝐾))
221220iftrued 4471 . . . . . . . . . . . . . 14 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0) = ((𝐵𝐾) − (𝐴𝐾)))
222221eqcomd 2824 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝐵𝐾) − (𝐴𝐾)) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
2236, 49resubcld 11056 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℝ)
224223recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑌 − (𝐴𝐾)) ∈ ℂ)
22577, 6resubcld 11056 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℝ)
226225recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐾) − 𝑌) ∈ ℂ)
227224, 226addcomd 10830 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))))
22877recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐾) ∈ ℂ)
2296recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑𝑌 ∈ ℂ)
23049recnd 10657 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴𝐾) ∈ ℂ)
231228, 229, 230npncand 11009 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐵𝐾) − 𝑌) + (𝑌 − (𝐴𝐾))) = ((𝐵𝐾) − (𝐴𝐾)))
232227, 231eqtrd 2853 . . . . . . . . . . . . . 14 (𝜑 → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
233232ad2antrr 722 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = ((𝐵𝐾) − (𝐴𝐾)))
234 volico 42145 . . . . . . . . . . . . . 14 (((𝐴𝐾) ∈ ℝ ∧ (𝐵𝐾) ∈ ℝ) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
235215, 217, 234syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = if((𝐴𝐾) < (𝐵𝐾), ((𝐵𝐾) − (𝐴𝐾)), 0))
236222, 233, 2353eqtr4d 2863 . . . . . . . . . . . 12 (((𝜑𝑌 < (𝐵𝐾)) ∧ (𝐴𝐾) < 𝑌) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
237190, 196, 236syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((𝑌 − (𝐴𝐾)) + ((𝐵𝐾) − 𝑌)) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
238189, 214, 2373eqtrd 2857 . . . . . . . . . 10 (((𝜑𝑌 < (𝐵𝐾)) ∧ ¬ 𝑌 ≤ (𝐴𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
239186, 238pm2.61dan 809 . . . . . . . . 9 ((𝜑𝑌 < (𝐵𝐾)) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
240163, 168, 239syl2anc 584 . . . . . . . 8 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)𝑌)) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
241162, 240eqtrd 2853 . . . . . . 7 ((𝜑 ∧ ¬ (𝐵𝐾) ≤ 𝑌) → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
242157, 241pm2.61dan 809 . . . . . 6 (𝜑 → ((vol‘((𝐴𝐾)[,)if((𝐵𝐾) ≤ 𝑌, (𝐵𝐾), 𝑌))) + (vol‘(if(𝑌 ≤ (𝐴𝐾), (𝐴𝐾), 𝑌)[,)(𝐵𝐾)))) = (vol‘((𝐴𝐾)[,)(𝐵𝐾))))
243115, 242eqtr2d 2854 . . . . 5 (𝜑 → (vol‘((𝐴𝐾)[,)(𝐵𝐾))) = ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾)))))
244243oveq2d 7161 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(𝐵𝐾)))) = (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
24532, 96fprodcl 15294 . . . . 5 (𝜑 → ∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) ∈ ℂ)
246245, 53, 80adddid 10653 . . . 4 (𝜑 → (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · ((vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾))) + (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))))
247103, 244, 2463eqtrrd 2858 . . 3 (𝜑 → ((∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((𝐴𝐾)[,)(((𝑇𝑌)‘𝐵)‘𝐾)))) + (∏𝑘 ∈ (𝑋 ∖ {𝐾})(vol‘((𝐴𝑘)[,)(𝐵𝑘))) · (vol‘((((𝑆𝑌)‘𝐴)‘𝐾)[,)(𝐵𝐾))))) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
24820, 93, 2473eqtrd 2857 . 2 (𝜑 → ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) + (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
2492, 3, 17, 4, 7hoidmvn0val 42743 . . 3 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))))
250249eqcomd 2824 . 2 (𝜑 → ∏𝑘𝑋 (vol‘((𝐴𝑘)[,)(𝐵𝑘))) = (𝐴(𝐿𝑋)𝐵))
25115, 248, 2503eqtrrd 2858 1 (𝜑 → (𝐴(𝐿𝑋)𝐵) = ((𝐴(𝐿𝑋)((𝑇𝑌)‘𝐵)) +𝑒 (((𝑆𝑌)‘𝐴)(𝐿𝑋)𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wne 3013  cdif 3930  cun 3931  wss 3933  c0 4288  ifcif 4463  {csn 4557   class class class wbr 5057  cmpt 5137  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  m cmap 8395  Fincfn 8497  cc 10523  cr 10524  0cc0 10525   + caddc 10528   · cmul 10530  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664  cmin 10858   +𝑒 cxad 12493  [,)cico 12728  cprod 15247  volcvol 23991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-er 8278  df-map 8397  df-pm 8398  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-n0 11886  df-z 11970  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-clim 14833  df-rlim 14834  df-sum 15031  df-prod 15248  df-rest 16684  df-topgen 16705  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-top 21430  df-topon 21447  df-bases 21482  df-cmp 21923  df-ovol 23992  df-vol 23993
This theorem is referenced by:  hspmbllem2  42786
  Copyright terms: Public domain W3C validator