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 44957
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 13382 . . . 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 44907 . . . . 5 (πœ‘ β†’ ((π‘‡β€˜π‘Œ)β€˜π΅):π‘‹βŸΆβ„)
92, 3, 4, 8hoidmvcl 44913 . . . 4 (πœ‘ β†’ (𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) ∈ (0[,)+∞))
101, 9sselid 3946 . . 3 (πœ‘ β†’ (𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) ∈ ℝ)
11 hspmbllem1.s . . . . . 6 𝑆 = (π‘₯ ∈ ℝ ↦ (𝑐 ∈ (ℝ ↑m 𝑋) ↦ (β„Ž ∈ 𝑋 ↦ if(β„Ž = 𝐾, if(π‘₯ ≀ (π‘β€˜β„Ž), (π‘β€˜β„Ž), π‘₯), (π‘β€˜β„Ž)))))
1211, 6, 3, 4hoidifhspf 44949 . . . . 5 (πœ‘ β†’ ((π‘†β€˜π‘Œ)β€˜π΄):π‘‹βŸΆβ„)
132, 3, 12, 7hoidmvcl 44913 . . . 4 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡) ∈ (0[,)+∞))
141, 13sselid 3946 . . 3 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡) ∈ ℝ)
1510, 14rexaddd 13162 . 2 (πœ‘ β†’ ((𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) +𝑒 (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡)) = ((𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) + (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡)))
16 hspmbllem1.k . . . . . 6 (πœ‘ β†’ 𝐾 ∈ 𝑋)
1716ne0d 4299 . . . . 5 (πœ‘ β†’ 𝑋 β‰  βˆ…)
182, 3, 17, 4, 8hoidmvn0val 44915 . . . 4 (πœ‘ β†’ (𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) = βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))))
192, 3, 17, 12, 7hoidmvn0val 44915 . . . 4 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡) = βˆπ‘˜ ∈ 𝑋 (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))))
2018, 19oveq12d 7379 . . 3 (πœ‘ β†’ ((𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) + (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡)) = (βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) + βˆπ‘˜ ∈ 𝑋 (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜)))))
21 uncom 4117 . . . . . . . . 9 ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ({𝐾} βˆͺ (𝑋 βˆ– {𝐾}))
2221a1i 11 . . . . . . . 8 (πœ‘ β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})))
2316snssd 4773 . . . . . . . . 9 (πœ‘ β†’ {𝐾} βŠ† 𝑋)
24 undif 4445 . . . . . . . . 9 ({𝐾} βŠ† 𝑋 ↔ ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})) = 𝑋)
2523, 24sylib 217 . . . . . . . 8 (πœ‘ β†’ ({𝐾} βˆͺ (𝑋 βˆ– {𝐾})) = 𝑋)
2622, 25eqtrd 2773 . . . . . . 7 (πœ‘ β†’ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}) = 𝑋)
2726eqcomd 2739 . . . . . 6 (πœ‘ β†’ 𝑋 = ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾}))
2827prodeq1d 15812 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))))
29 nfv 1918 . . . . . 6 β„²π‘˜πœ‘
30 nfcv 2904 . . . . . 6 β„²π‘˜(volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))
31 difssd 4096 . . . . . . 7 (πœ‘ β†’ (𝑋 βˆ– {𝐾}) βŠ† 𝑋)
323, 31ssfid 9217 . . . . . 6 (πœ‘ β†’ (𝑋 βˆ– {𝐾}) ∈ Fin)
33 neldifsnd 4757 . . . . . 6 (πœ‘ β†’ Β¬ 𝐾 ∈ (𝑋 βˆ– {𝐾}))
344adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ 𝐴:π‘‹βŸΆβ„)
3531sselda 3948 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ π‘˜ ∈ 𝑋)
3634, 35ffvelcdmd 7040 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (π΄β€˜π‘˜) ∈ ℝ)
376adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ π‘Œ ∈ ℝ)
383adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ 𝑋 ∈ Fin)
397adantr 482 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ 𝐡:π‘‹βŸΆβ„)
405, 37, 38, 39hsphoif 44907 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ ((π‘‡β€˜π‘Œ)β€˜π΅):π‘‹βŸΆβ„)
4140, 35ffvelcdmd 7040 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜) ∈ ℝ)
42 volicore 44912 . . . . . . . 8 (((π΄β€˜π‘˜) ∈ ℝ ∧ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜) ∈ ℝ) β†’ (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) ∈ ℝ)
4336, 41, 42syl2anc 585 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) ∈ ℝ)
4443recnd 11191 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) ∈ β„‚)
45 fveq2 6846 . . . . . . . 8 (π‘˜ = 𝐾 β†’ (π΄β€˜π‘˜) = (π΄β€˜πΎ))
46 fveq2 6846 . . . . . . . 8 (π‘˜ = 𝐾 β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜) = (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))
4745, 46oveq12d 7379 . . . . . . 7 (π‘˜ = 𝐾 β†’ ((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜)) = ((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))
4847fveq2d 6850 . . . . . 6 (π‘˜ = 𝐾 β†’ (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))))
494, 16ffvelcdmd 7040 . . . . . . . 8 (πœ‘ β†’ (π΄β€˜πΎ) ∈ ℝ)
508, 16ffvelcdmd 7040 . . . . . . . 8 (πœ‘ β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ) ∈ ℝ)
51 volicore 44912 . . . . . . . 8 (((π΄β€˜πΎ) ∈ ℝ ∧ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ) ∈ ℝ) β†’ (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) ∈ ℝ)
5249, 50, 51syl2anc 585 . . . . . . 7 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) ∈ ℝ)
5352recnd 11191 . . . . . 6 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) ∈ β„‚)
5429, 30, 32, 16, 33, 44, 48, 53fprodsplitsn 15880 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))))
555, 37, 38, 39, 35hsphoival 44910 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜) = if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), (π΅β€˜π‘˜), if((π΅β€˜π‘˜) ≀ π‘Œ, (π΅β€˜π‘˜), π‘Œ)))
56 iftrue 4496 . . . . . . . . . . 11 (π‘˜ ∈ (𝑋 βˆ– {𝐾}) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), (π΅β€˜π‘˜), if((π΅β€˜π‘˜) ≀ π‘Œ, (π΅β€˜π‘˜), π‘Œ)) = (π΅β€˜π‘˜))
5756adantl 483 . . . . . . . . . 10 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ if(π‘˜ ∈ (𝑋 βˆ– {𝐾}), (π΅β€˜π‘˜), if((π΅β€˜π‘˜) ≀ π‘Œ, (π΅β€˜π‘˜), π‘Œ)) = (π΅β€˜π‘˜))
5855, 57eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜) = (π΅β€˜π‘˜))
5958oveq2d 7377 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ ((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜)) = ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)))
6059fveq2d 6850 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
6160prodeq2dv 15814 . . . . . 6 (πœ‘ β†’ βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
6261oveq1d 7376 . . . . 5 (πœ‘ β†’ (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))))
6328, 54, 623eqtrd 2777 . . . 4 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))))
6427prodeq1d 15812 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))))
65 nfcv 2904 . . . . . 6 β„²π‘˜(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))
6612adantr 482 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ ((π‘†β€˜π‘Œ)β€˜π΄):π‘‹βŸΆβ„)
6766, 35ffvelcdmd 7040 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜) ∈ ℝ)
6858, 41eqeltrrd 2835 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (π΅β€˜π‘˜) ∈ ℝ)
69 volicore 44912 . . . . . . . 8 (((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜) ∈ ℝ ∧ (π΅β€˜π‘˜) ∈ ℝ) β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) ∈ ℝ)
7067, 68, 69syl2anc 585 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) ∈ ℝ)
7170recnd 11191 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) ∈ β„‚)
72 fveq2 6846 . . . . . . . 8 (π‘˜ = 𝐾 β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜) = (((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ))
73 fveq2 6846 . . . . . . . 8 (π‘˜ = 𝐾 β†’ (π΅β€˜π‘˜) = (π΅β€˜πΎ))
7472, 73oveq12d 7379 . . . . . . 7 (π‘˜ = 𝐾 β†’ ((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜)) = ((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))
7574fveq2d 6850 . . . . . 6 (π‘˜ = 𝐾 β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))
7612, 16ffvelcdmd 7040 . . . . . . . 8 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ) ∈ ℝ)
777, 16ffvelcdmd 7040 . . . . . . . 8 (πœ‘ β†’ (π΅β€˜πΎ) ∈ ℝ)
78 volicore 44912 . . . . . . . 8 (((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ) ∈ ℝ ∧ (π΅β€˜πΎ) ∈ ℝ) β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ ℝ)
7976, 77, 78syl2anc 585 . . . . . . 7 (πœ‘ β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ ℝ)
8079recnd 11191 . . . . . 6 (πœ‘ β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ β„‚)
8129, 65, 32, 16, 33, 71, 75, 80fprodsplitsn 15880 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))))
8211, 37, 38, 34, 35hoidifhspval3 44950 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜) = if(π‘˜ = 𝐾, if(π‘Œ ≀ (π΄β€˜π‘˜), (π΄β€˜π‘˜), π‘Œ), (π΄β€˜π‘˜)))
83 eldifsni 4754 . . . . . . . . . . . 12 (π‘˜ ∈ (𝑋 βˆ– {𝐾}) β†’ π‘˜ β‰  𝐾)
84 neneq 2946 . . . . . . . . . . . 12 (π‘˜ β‰  𝐾 β†’ Β¬ π‘˜ = 𝐾)
8583, 84syl 17 . . . . . . . . . . 11 (π‘˜ ∈ (𝑋 βˆ– {𝐾}) β†’ Β¬ π‘˜ = 𝐾)
8685iffalsed 4501 . . . . . . . . . 10 (π‘˜ ∈ (𝑋 βˆ– {𝐾}) β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ (π΄β€˜π‘˜), (π΄β€˜π‘˜), π‘Œ), (π΄β€˜π‘˜)) = (π΄β€˜π‘˜))
8786adantl 483 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ if(π‘˜ = 𝐾, if(π‘Œ ≀ (π΄β€˜π‘˜), (π΄β€˜π‘˜), π‘Œ), (π΄β€˜π‘˜)) = (π΄β€˜π‘˜))
8882, 87eqtrd 2773 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜) = (π΄β€˜π‘˜))
8988fvoveq1d 7383 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
9089prodeq2dv 15814 . . . . . 6 (πœ‘ β†’ βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
9190oveq1d 7376 . . . . 5 (πœ‘ β†’ (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))))
9264, 81, 913eqtrd 2777 . . . 4 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))))
9363, 92oveq12d 7379 . . 3 (πœ‘ β†’ (βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜π‘˜))) + βˆπ‘˜ ∈ 𝑋 (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜π‘˜)[,)(π΅β€˜π‘˜)))) = ((βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))) + (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))))
9427prodeq1d 15812 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) = βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
95 nfcv 2904 . . . . . 6 β„²π‘˜(volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))
9660, 44eqeltrrd 2835 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ (𝑋 βˆ– {𝐾})) β†’ (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) ∈ β„‚)
9745, 73oveq12d 7379 . . . . . . 7 (π‘˜ = 𝐾 β†’ ((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜)) = ((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))
9897fveq2d 6850 . . . . . 6 (π‘˜ = 𝐾 β†’ (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
99 volicore 44912 . . . . . . . 8 (((π΄β€˜πΎ) ∈ ℝ ∧ (π΅β€˜πΎ) ∈ ℝ) β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ ℝ)
10049, 77, 99syl2anc 585 . . . . . . 7 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ ℝ)
101100recnd 11191 . . . . . 6 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) ∈ β„‚)
10229, 95, 32, 16, 33, 96, 98, 101fprodsplitsn 15880 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ ((𝑋 βˆ– {𝐾}) βˆͺ {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
10394, 102eqtrd 2773 . . . 4 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
1045, 6, 3, 7, 16hsphoival 44910 . . . . . . . . . 10 (πœ‘ β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ) = if(𝐾 ∈ (𝑋 βˆ– {𝐾}), (π΅β€˜πΎ), if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ)))
10533iffalsed 4501 . . . . . . . . . 10 (πœ‘ β†’ if(𝐾 ∈ (𝑋 βˆ– {𝐾}), (π΅β€˜πΎ), if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ)) = if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))
106104, 105eqtrd 2773 . . . . . . . . 9 (πœ‘ β†’ (((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ) = if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))
107106oveq2d 7377 . . . . . . . 8 (πœ‘ β†’ ((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)) = ((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ)))
108107fveq2d 6850 . . . . . . 7 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) = (volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))))
10911, 6, 3, 4, 16hoidifhspval3 44950 . . . . . . . . 9 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ) = if(𝐾 = 𝐾, if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ), (π΄β€˜πΎ)))
110 eqid 2733 . . . . . . . . . . 11 𝐾 = 𝐾
111110iftruei 4497 . . . . . . . . . 10 if(𝐾 = 𝐾, if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ), (π΄β€˜πΎ)) = if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)
112111a1i 11 . . . . . . . . 9 (πœ‘ β†’ if(𝐾 = 𝐾, if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ), (π΄β€˜πΎ)) = if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ))
113109, 112eqtrd 2773 . . . . . . . 8 (πœ‘ β†’ (((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ) = if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ))
114113fvoveq1d 7383 . . . . . . 7 (πœ‘ β†’ (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))) = (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ))))
115108, 114oveq12d 7379 . . . . . 6 (πœ‘ β†’ ((volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) + (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))))
116 iftrue 4496 . . . . . . . . . . . 12 ((π΅β€˜πΎ) ≀ π‘Œ β†’ if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ) = (π΅β€˜πΎ))
117116oveq2d 7377 . . . . . . . . . . 11 ((π΅β€˜πΎ) ≀ π‘Œ β†’ ((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ)) = ((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))
118117fveq2d 6850 . . . . . . . . . 10 ((π΅β€˜πΎ) ≀ π‘Œ β†’ (volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
119118oveq1d 7376 . . . . . . . . 9 ((π΅β€˜πΎ) ≀ π‘Œ β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))))
120119adantl 483 . . . . . . . 8 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))))
121 iftrue 4496 . . . . . . . . . . . . . . 15 (π‘Œ ≀ (π΄β€˜πΎ) β†’ if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ) = (π΄β€˜πΎ))
122121oveq1d 7376 . . . . . . . . . . . . . 14 (π‘Œ ≀ (π΄β€˜πΎ) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = ((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))
123122adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = ((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))
12477ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΅β€˜πΎ) ∈ ℝ)
1256ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ π‘Œ ∈ ℝ)
12649ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) ∈ ℝ)
127 simplr 768 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΅β€˜πΎ) ≀ π‘Œ)
128 simpr 486 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ π‘Œ ≀ (π΄β€˜πΎ))
129124, 125, 126, 127, 128letrd 11320 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΅β€˜πΎ) ≀ (π΄β€˜πΎ))
130126rexrd 11213 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) ∈ ℝ*)
131124rexrd 11213 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΅β€˜πΎ) ∈ ℝ*)
132 ico0 13319 . . . . . . . . . . . . . . 15 (((π΄β€˜πΎ) ∈ ℝ* ∧ (π΅β€˜πΎ) ∈ ℝ*) β†’ (((π΄β€˜πΎ)[,)(π΅β€˜πΎ)) = βˆ… ↔ (π΅β€˜πΎ) ≀ (π΄β€˜πΎ)))
133130, 131, 132syl2anc 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (((π΄β€˜πΎ)[,)(π΅β€˜πΎ)) = βˆ… ↔ (π΅β€˜πΎ) ≀ (π΄β€˜πΎ)))
134129, 133mpbird 257 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((π΄β€˜πΎ)[,)(π΅β€˜πΎ)) = βˆ…)
135123, 134eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = βˆ…)
136 iffalse 4499 . . . . . . . . . . . . . . 15 (Β¬ π‘Œ ≀ (π΄β€˜πΎ) β†’ if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ) = π‘Œ)
137136oveq1d 7376 . . . . . . . . . . . . . 14 (Β¬ π‘Œ ≀ (π΄β€˜πΎ) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = (π‘Œ[,)(π΅β€˜πΎ)))
138137adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = (π‘Œ[,)(π΅β€˜πΎ)))
139 simpr 486 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (π΅β€˜πΎ) ≀ π‘Œ)
1406rexrd 11213 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ π‘Œ ∈ ℝ*)
141140adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ π‘Œ ∈ ℝ*)
14277rexrd 11213 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π΅β€˜πΎ) ∈ ℝ*)
143142adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (π΅β€˜πΎ) ∈ ℝ*)
144 ico0 13319 . . . . . . . . . . . . . . . 16 ((π‘Œ ∈ ℝ* ∧ (π΅β€˜πΎ) ∈ ℝ*) β†’ ((π‘Œ[,)(π΅β€˜πΎ)) = βˆ… ↔ (π΅β€˜πΎ) ≀ π‘Œ))
145141, 143, 144syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((π‘Œ[,)(π΅β€˜πΎ)) = βˆ… ↔ (π΅β€˜πΎ) ≀ π‘Œ))
146139, 145mpbird 257 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (π‘Œ[,)(π΅β€˜πΎ)) = βˆ…)
147146adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π‘Œ[,)(π΅β€˜πΎ)) = βˆ…)
148138, 147eqtrd 2773 . . . . . . . . . . . 12 (((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = βˆ…)
149135, 148pm2.61dan 812 . . . . . . . . . . 11 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)) = βˆ…)
150149fveq2d 6850 . . . . . . . . . 10 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ))) = (volβ€˜βˆ…))
151 vol0 44290 . . . . . . . . . . 11 (volβ€˜βˆ…) = 0
152151a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (volβ€˜βˆ…) = 0)
153150, 152eqtrd 2773 . . . . . . . . 9 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ))) = 0)
154153oveq2d 7377 . . . . . . . 8 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + 0))
155101addridd 11363 . . . . . . . . 9 (πœ‘ β†’ ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + 0) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
156155adantr 482 . . . . . . . 8 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) + 0) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
157120, 154, 1563eqtrd 2777 . . . . . . 7 ((πœ‘ ∧ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
158 iffalse 4499 . . . . . . . . . . . 12 (Β¬ (π΅β€˜πΎ) ≀ π‘Œ β†’ if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ) = π‘Œ)
159158oveq2d 7377 . . . . . . . . . . 11 (Β¬ (π΅β€˜πΎ) ≀ π‘Œ β†’ ((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ)) = ((π΄β€˜πΎ)[,)π‘Œ))
160159fveq2d 6850 . . . . . . . . . 10 (Β¬ (π΅β€˜πΎ) ≀ π‘Œ β†’ (volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) = (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)))
161160adantl 483 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) = (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)))
162161oveq1d 7376 . . . . . . . 8 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))))
163 simpl 484 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ πœ‘)
164 simpr 486 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ Β¬ (π΅β€˜πΎ) ≀ π‘Œ)
165163, 6syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ π‘Œ ∈ ℝ)
166163, 77syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (π΅β€˜πΎ) ∈ ℝ)
167165, 166ltnled 11310 . . . . . . . . . 10 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ (π‘Œ < (π΅β€˜πΎ) ↔ Β¬ (π΅β€˜πΎ) ≀ π‘Œ))
168164, 167mpbird 257 . . . . . . . . 9 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ π‘Œ < (π΅β€˜πΎ))
169121fvoveq1d 7383 . . . . . . . . . . . . 13 (π‘Œ ≀ (π΄β€˜πΎ) β†’ (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
170169oveq2d 7377 . . . . . . . . . . . 12 (π‘Œ ≀ (π΄β€˜πΎ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
171170adantl 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
172 simpr 486 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ π‘Œ ≀ (π΄β€˜πΎ))
17349rexrd 11213 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (π΄β€˜πΎ) ∈ ℝ*)
174173adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) ∈ ℝ*)
175140adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ π‘Œ ∈ ℝ*)
176 ico0 13319 . . . . . . . . . . . . . . . . 17 (((π΄β€˜πΎ) ∈ ℝ* ∧ π‘Œ ∈ ℝ*) β†’ (((π΄β€˜πΎ)[,)π‘Œ) = βˆ… ↔ π‘Œ ≀ (π΄β€˜πΎ)))
177174, 175, 176syl2anc 585 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (((π΄β€˜πΎ)[,)π‘Œ) = βˆ… ↔ π‘Œ ≀ (π΄β€˜πΎ)))
178172, 177mpbird 257 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((π΄β€˜πΎ)[,)π‘Œ) = βˆ…)
179178fveq2d 6850 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = (volβ€˜βˆ…))
180151a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (volβ€˜βˆ…) = 0)
181179, 180eqtrd 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = 0)
182181oveq1d 7376 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))) = (0 + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
183182adantlr 714 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))) = (0 + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))))
184101addlidd 11364 . . . . . . . . . . . 12 (πœ‘ β†’ (0 + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
185184ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (0 + (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
186171, 183, 1853eqtrd 2777 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
187136fvoveq1d 7383 . . . . . . . . . . . . 13 (Β¬ π‘Œ ≀ (π΄β€˜πΎ) β†’ (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ))) = (volβ€˜(π‘Œ[,)(π΅β€˜πΎ))))
188187oveq2d 7377 . . . . . . . . . . . 12 (Β¬ π‘Œ ≀ (π΄β€˜πΎ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(π‘Œ[,)(π΅β€˜πΎ)))))
189188adantl 483 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(π‘Œ[,)(π΅β€˜πΎ)))))
190 simpl 484 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)))
191 simpr 486 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ Β¬ π‘Œ ≀ (π΄β€˜πΎ))
19249adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) ∈ ℝ)
1936adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ π‘Œ ∈ ℝ)
194192, 193ltnled 11310 . . . . . . . . . . . . . 14 ((πœ‘ ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((π΄β€˜πΎ) < π‘Œ ↔ Β¬ π‘Œ ≀ (π΄β€˜πΎ)))
195191, 194mpbird 257 . . . . . . . . . . . . 13 ((πœ‘ ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) < π‘Œ)
196195adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ (π΄β€˜πΎ) < π‘Œ)
19749adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (π΄β€˜πΎ) ∈ ℝ)
1986adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ (π΄β€˜πΎ) < π‘Œ) β†’ π‘Œ ∈ ℝ)
199 volico 44314 . . . . . . . . . . . . . . . 16 (((π΄β€˜πΎ) ∈ ℝ ∧ π‘Œ ∈ ℝ) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = if((π΄β€˜πΎ) < π‘Œ, (π‘Œ βˆ’ (π΄β€˜πΎ)), 0))
200197, 198, 199syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = if((π΄β€˜πΎ) < π‘Œ, (π‘Œ βˆ’ (π΄β€˜πΎ)), 0))
201 iftrue 4496 . . . . . . . . . . . . . . . 16 ((π΄β€˜πΎ) < π‘Œ β†’ if((π΄β€˜πΎ) < π‘Œ, (π‘Œ βˆ’ (π΄β€˜πΎ)), 0) = (π‘Œ βˆ’ (π΄β€˜πΎ)))
202201adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (π΄β€˜πΎ) < π‘Œ) β†’ if((π΄β€˜πΎ) < π‘Œ, (π‘Œ βˆ’ (π΄β€˜πΎ)), 0) = (π‘Œ βˆ’ (π΄β€˜πΎ)))
203200, 202eqtrd 2773 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = (π‘Œ βˆ’ (π΄β€˜πΎ)))
204203adantlr 714 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) = (π‘Œ βˆ’ (π΄β€˜πΎ)))
2056adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ π‘Œ ∈ ℝ)
20677adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ (π΅β€˜πΎ) ∈ ℝ)
207 volico 44314 . . . . . . . . . . . . . . . 16 ((π‘Œ ∈ ℝ ∧ (π΅β€˜πΎ) ∈ ℝ) β†’ (volβ€˜(π‘Œ[,)(π΅β€˜πΎ))) = if(π‘Œ < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ π‘Œ), 0))
208205, 206, 207syl2anc 585 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ (volβ€˜(π‘Œ[,)(π΅β€˜πΎ))) = if(π‘Œ < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ π‘Œ), 0))
209 iftrue 4496 . . . . . . . . . . . . . . . 16 (π‘Œ < (π΅β€˜πΎ) β†’ if(π‘Œ < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ π‘Œ), 0) = ((π΅β€˜πΎ) βˆ’ π‘Œ))
210209adantl 483 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ if(π‘Œ < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ π‘Œ), 0) = ((π΅β€˜πΎ) βˆ’ π‘Œ))
211208, 210eqtrd 2773 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ (volβ€˜(π‘Œ[,)(π΅β€˜πΎ))) = ((π΅β€˜πΎ) βˆ’ π‘Œ))
212211adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (volβ€˜(π‘Œ[,)(π΅β€˜πΎ))) = ((π΅β€˜πΎ) βˆ’ π‘Œ))
213204, 212oveq12d 7379 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(π‘Œ[,)(π΅β€˜πΎ)))) = ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)))
214190, 196, 213syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(π‘Œ[,)(π΅β€˜πΎ)))) = ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)))
215197adantlr 714 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (π΄β€˜πΎ) ∈ ℝ)
216205adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ π‘Œ ∈ ℝ)
217206adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (π΅β€˜πΎ) ∈ ℝ)
218 simpr 486 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (π΄β€˜πΎ) < π‘Œ)
219 simplr 768 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ π‘Œ < (π΅β€˜πΎ))
220215, 216, 217, 218, 219lttrd 11324 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (π΄β€˜πΎ) < (π΅β€˜πΎ))
221220iftrued 4498 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ if((π΄β€˜πΎ) < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)), 0) = ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)))
222221eqcomd 2739 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)) = if((π΄β€˜πΎ) < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)), 0))
2236, 49resubcld 11591 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (π‘Œ βˆ’ (π΄β€˜πΎ)) ∈ ℝ)
224223recnd 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π‘Œ βˆ’ (π΄β€˜πΎ)) ∈ β„‚)
22577, 6resubcld 11591 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((π΅β€˜πΎ) βˆ’ π‘Œ) ∈ ℝ)
226225recnd 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((π΅β€˜πΎ) βˆ’ π‘Œ) ∈ β„‚)
227224, 226addcomd 11365 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)) = (((π΅β€˜πΎ) βˆ’ π‘Œ) + (π‘Œ βˆ’ (π΄β€˜πΎ))))
22877recnd 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π΅β€˜πΎ) ∈ β„‚)
2296recnd 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ π‘Œ ∈ β„‚)
23049recnd 11191 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (π΄β€˜πΎ) ∈ β„‚)
231228, 229, 230npncand 11544 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (((π΅β€˜πΎ) βˆ’ π‘Œ) + (π‘Œ βˆ’ (π΄β€˜πΎ))) = ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)))
232227, 231eqtrd 2773 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)) = ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)))
233232ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)) = ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)))
234 volico 44314 . . . . . . . . . . . . . 14 (((π΄β€˜πΎ) ∈ ℝ ∧ (π΅β€˜πΎ) ∈ ℝ) β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) = if((π΄β€˜πΎ) < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)), 0))
235215, 217, 234syl2anc 585 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) = if((π΄β€˜πΎ) < (π΅β€˜πΎ), ((π΅β€˜πΎ) βˆ’ (π΄β€˜πΎ)), 0))
236222, 233, 2353eqtr4d 2783 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ (π΄β€˜πΎ) < π‘Œ) β†’ ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
237190, 196, 236syl2anc 585 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((π‘Œ βˆ’ (π΄β€˜πΎ)) + ((π΅β€˜πΎ) βˆ’ π‘Œ)) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
238189, 214, 2373eqtrd 2777 . . . . . . . . . 10 (((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) ∧ Β¬ π‘Œ ≀ (π΄β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
239186, 238pm2.61dan 812 . . . . . . . . 9 ((πœ‘ ∧ π‘Œ < (π΅β€˜πΎ)) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
240163, 168, 239syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)π‘Œ)) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
241162, 240eqtrd 2773 . . . . . . 7 ((πœ‘ ∧ Β¬ (π΅β€˜πΎ) ≀ π‘Œ) β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
242157, 241pm2.61dan 812 . . . . . 6 (πœ‘ β†’ ((volβ€˜((π΄β€˜πΎ)[,)if((π΅β€˜πΎ) ≀ π‘Œ, (π΅β€˜πΎ), π‘Œ))) + (volβ€˜(if(π‘Œ ≀ (π΄β€˜πΎ), (π΄β€˜πΎ), π‘Œ)[,)(π΅β€˜πΎ)))) = (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))))
243115, 242eqtr2d 2774 . . . . 5 (πœ‘ β†’ (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ))) = ((volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) + (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ)))))
244243oveq2d 7377 . . . 4 (πœ‘ β†’ (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(π΅β€˜πΎ)))) = (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· ((volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) + (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))))
24532, 96fprodcl 15843 . . . . 5 (πœ‘ β†’ βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) ∈ β„‚)
246245, 53, 80adddid 11187 . . . 4 (πœ‘ β†’ (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· ((volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ))) + (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))) = ((βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))) + (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))))
247103, 244, 2463eqtrrd 2778 . . 3 (πœ‘ β†’ ((βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((π΄β€˜πΎ)[,)(((π‘‡β€˜π‘Œ)β€˜π΅)β€˜πΎ)))) + (βˆπ‘˜ ∈ (𝑋 βˆ– {𝐾})(volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) Β· (volβ€˜((((π‘†β€˜π‘Œ)β€˜π΄)β€˜πΎ)[,)(π΅β€˜πΎ))))) = βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
24820, 93, 2473eqtrd 2777 . 2 (πœ‘ β†’ ((𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) + (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡)) = βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
2492, 3, 17, 4, 7hoidmvn0val 44915 . . 3 (πœ‘ β†’ (𝐴(πΏβ€˜π‘‹)𝐡) = βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))))
250249eqcomd 2739 . 2 (πœ‘ β†’ βˆπ‘˜ ∈ 𝑋 (volβ€˜((π΄β€˜π‘˜)[,)(π΅β€˜π‘˜))) = (𝐴(πΏβ€˜π‘‹)𝐡))
25115, 248, 2503eqtrrd 2778 1 (πœ‘ β†’ (𝐴(πΏβ€˜π‘‹)𝐡) = ((𝐴(πΏβ€˜π‘‹)((π‘‡β€˜π‘Œ)β€˜π΅)) +𝑒 (((π‘†β€˜π‘Œ)β€˜π΄)(πΏβ€˜π‘‹)𝐡)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107   β‰  wne 2940   βˆ– cdif 3911   βˆͺ cun 3912   βŠ† wss 3914  βˆ…c0 4286  ifcif 4490  {csn 4590   class class class wbr 5109   ↦ cmpt 5192  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361   ∈ cmpo 7363   ↑m cmap 8771  Fincfn 8889  β„‚cc 11057  β„cr 11058  0cc0 11059   + caddc 11062   Β· cmul 11064  +∞cpnf 11194  β„*cxr 11196   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   +𝑒 cxad 13039  [,)cico 13275  βˆcprod 15796  volcvol 24850
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-of 7621  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-er 8654  df-map 8773  df-pm 8774  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-fi 9355  df-sup 9386  df-inf 9387  df-oi 9454  df-dju 9845  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-q 12882  df-rp 12924  df-xneg 13041  df-xadd 13042  df-xmul 13043  df-ioo 13277  df-ico 13279  df-icc 13280  df-fz 13434  df-fzo 13577  df-fl 13706  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-rlim 15380  df-sum 15580  df-prod 15797  df-rest 17312  df-topgen 17333  df-psmet 20811  df-xmet 20812  df-met 20813  df-bl 20814  df-mopn 20815  df-top 22266  df-topon 22283  df-bases 22319  df-cmp 22761  df-ovol 24851  df-vol 24852
This theorem is referenced by:  hspmbllem2  44958
  Copyright terms: Public domain W3C validator