MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfmulc2lem Structured version   Visualization version   GIF version
Theorem mbfmulc2lem 25155
Description: Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014.)
Hypotheses
Ref Expression
mbfmulc2re.1 (πœ‘ β†’ 𝐹 ∈ MblFn)
mbfmulc2re.2 (πœ‘ β†’ 𝐡 ∈ ℝ)
mbfmulc2lem.3 (πœ‘ β†’ 𝐹:π΄βŸΆβ„)
Assertion
Ref Expression
mbfmulc2lem (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
Proof of Theorem mbfmulc2lem
Dummy variables π‘₯ 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 remulcl 11191 . . . . . 6 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
21adantl 482 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
3 mbfmulc2re.2 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
4 fconst6g 6777 . . . . . 6 (𝐡 ∈ ℝ β†’ (𝐴 Γ— {𝐡}):π΄βŸΆβ„)
53, 4syl 17 . . . . 5 (πœ‘ β†’ (𝐴 Γ— {𝐡}):π΄βŸΆβ„)
6 mbfmulc2lem.3 . . . . 5 (πœ‘ β†’ 𝐹:π΄βŸΆβ„)
76fdmd 6725 . . . . . 6 (πœ‘ β†’ dom 𝐹 = 𝐴)
8 mbfmulc2re.1 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ MblFn)
9 mbfdm 25134 . . . . . . 7 (𝐹 ∈ MblFn β†’ dom 𝐹 ∈ dom vol)
108, 9syl 17 . . . . . 6 (πœ‘ β†’ dom 𝐹 ∈ dom vol)
117, 10eqeltrrd 2834 . . . . 5 (πœ‘ β†’ 𝐴 ∈ dom vol)
12 inidm 4217 . . . . 5 (𝐴 ∩ 𝐴) = 𝐴
132, 5, 6, 11, 11, 12off 7684 . . . 4 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
1413adantr 481 . . 3 ((πœ‘ ∧ 𝐡 < 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
1511adantr 481 . . 3 ((πœ‘ ∧ 𝐡 < 0) β†’ 𝐴 ∈ dom vol)
16 simprl 769 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ)
1716rexrd 11260 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ*)
18 elioopnf 13416 . . . . . . . . . 10 (𝑦 ∈ ℝ* β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
1917, 18syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
2013ffvelcdmda 7083 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
2120ad2ant2rl 747 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
2221biantrurd 533 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
236ffvelcdmda 7083 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) ∈ ℝ)
2423ad2ant2rl 747 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ ℝ)
2524biantrurd 533 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (𝑦 / 𝐡) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
26 simprr 771 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑧 ∈ 𝐴)
2711ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐴 ∈ dom vol)
283ad2antrr 724 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ)
296ad2antrr 724 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐹:π΄βŸΆβ„)
3029ffnd 6715 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐹 Fn 𝐴)
31 eqidd 2733 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
3227, 28, 30, 31ofc1 7692 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
3326, 32mpdan 685 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
3433breq2d 5159 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
3533, 21eqeltrrd 2834 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝐡 Β· (πΉβ€˜π‘§)) ∈ ℝ)
3616, 35ltnegd 11788 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (𝐡 Β· (πΉβ€˜π‘§)) ↔ -(𝐡 Β· (πΉβ€˜π‘§)) < -𝑦))
3728recnd 11238 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ β„‚)
3824recnd 11238 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ β„‚)
3937, 38mulneg1d 11663 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝐡 Β· (πΉβ€˜π‘§)) = -(𝐡 Β· (πΉβ€˜π‘§)))
4039breq1d 5157 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ -(𝐡 Β· (πΉβ€˜π‘§)) < -𝑦))
4116renegcld 11637 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ -𝑦 ∈ ℝ)
4228renegcld 11637 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ -𝐡 ∈ ℝ)
43 simplr 767 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 < 0)
4428lt0neg1d 11779 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝐡 < 0 ↔ 0 < -𝐡))
4543, 44mpbid 231 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 0 < -𝐡)
46 ltmuldiv2 12084 . . . . . . . . . . . . 13 (((πΉβ€˜π‘§) ∈ ℝ ∧ -𝑦 ∈ ℝ ∧ (-𝐡 ∈ ℝ ∧ 0 < -𝐡)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ (πΉβ€˜π‘§) < (-𝑦 / -𝐡)))
4724, 41, 42, 45, 46syl112anc 1374 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ (πΉβ€˜π‘§) < (-𝑦 / -𝐡)))
4836, 40, 473bitr2rd 307 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (-𝑦 / -𝐡) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
4916recnd 11238 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ β„‚)
5043lt0ne0d 11775 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 β‰  0)
5149, 37, 50div2negd 12001 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝑦 / -𝐡) = (𝑦 / 𝐡))
5251breq2d 5159 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (-𝑦 / -𝐡) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
5334, 48, 523bitr2d 306 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
5416, 28, 50redivcld 12038 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ)
5554rexrd 11260 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ*)
56 elioomnf 13417 . . . . . . . . . . 11 ((𝑦 / 𝐡) ∈ ℝ* β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
5755, 56syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
5825, 53, 573bitr4d 310 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
5919, 22, 583bitr2d 306 . . . . . . . 8 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
6059anassrs 468 . . . . . . 7 ((((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
6160pm5.32da 579 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
6213ffnd 6715 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
6362ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
64 elpreima 7056 . . . . . . 7 (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴 β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
6563, 64syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
666ffnd 6715 . . . . . . . 8 (πœ‘ β†’ 𝐹 Fn 𝐴)
6766ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ 𝐹 Fn 𝐴)
68 elpreima 7056 . . . . . . 7 (𝐹 Fn 𝐴 β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
6967, 68syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
7061, 65, 693bitr4d 310 . . . . 5 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡)))))
7170eqrdv 2730 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) = (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))))
72 mbfima 25138 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:π΄βŸΆβ„) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
738, 6, 72syl2anc 584 . . . . 5 (πœ‘ β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
7473ad2antrr 724 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
7571, 74eqeltrd 2833 . . 3 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ∈ dom vol)
76 elioomnf 13417 . . . . . . . . . 10 (𝑦 ∈ ℝ* β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7717, 76syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7821biantrurd 533 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7924biantrurd 533 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
8033breq1d 5157 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
8139breq2d 5159 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝑦 < (-𝐡 Β· (πΉβ€˜π‘§)) ↔ -𝑦 < -(𝐡 Β· (πΉβ€˜π‘§))))
8251breq1d 5157 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
83 ltdivmul 12085 . . . . . . . . . . . . . 14 ((-𝑦 ∈ ℝ ∧ (πΉβ€˜π‘§) ∈ ℝ ∧ (-𝐡 ∈ ℝ ∧ 0 < -𝐡)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8441, 24, 42, 45, 83syl112anc 1374 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8582, 84bitr3d 280 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8635, 16ltnegd 11788 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ -𝑦 < -(𝐡 Β· (πΉβ€˜π‘§))))
8781, 85, 863bitr4d 310 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
8880, 87bitr4d 281 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
89 elioopnf 13416 . . . . . . . . . . 11 ((𝑦 / 𝐡) ∈ ℝ* β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
9055, 89syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
9179, 88, 903bitr4d 310 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9277, 78, 913bitr2d 306 . . . . . . . 8 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9392anassrs 468 . . . . . . 7 ((((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9493pm5.32da 579 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
95 elpreima 7056 . . . . . . 7 (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴 β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
9663, 95syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
97 elpreima 7056 . . . . . . 7 (𝐹 Fn 𝐴 β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
9867, 97syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
9994, 96, 983bitr4d 310 . . . . 5 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ 𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞))))
10099eqrdv 2730 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) = (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)))
101 mbfima 25138 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:π΄βŸΆβ„) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
1028, 6, 101syl2anc 584 . . . . 5 (πœ‘ β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
103102ad2antrr 724 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
104100, 103eqeltrd 2833 . . 3 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ∈ dom vol)
10514, 15, 75, 104ismbf2d 25148 . 2 ((πœ‘ ∧ 𝐡 < 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
10611adantr 481 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐴 ∈ dom vol)
1076adantr 481 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐹:π΄βŸΆβ„)
108 simpr 485 . . . . 5 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐡 = 0)
109 0cn 11202 . . . . 5 0 ∈ β„‚
110108, 109eqeltrdi 2841 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐡 ∈ β„‚)
111 0cnd 11203 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 0 ∈ β„‚)
112 simplr 767 . . . . . 6 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ 𝐡 = 0)
113112oveq1d 7420 . . . . 5 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (𝐡 Β· π‘₯) = (0 Β· π‘₯))
114 mul02lem2 11387 . . . . . 6 (π‘₯ ∈ ℝ β†’ (0 Β· π‘₯) = 0)
115114adantl 482 . . . . 5 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (0 Β· π‘₯) = 0)
116113, 115eqtrd 2772 . . . 4 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (𝐡 Β· π‘₯) = 0)
117106, 107, 110, 111, 116caofid2 7700 . . 3 ((πœ‘ ∧ 𝐡 = 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) = (𝐴 Γ— {0}))
118 mbfconst 25141 . . . 4 ((𝐴 ∈ dom vol ∧ 0 ∈ β„‚) β†’ (𝐴 Γ— {0}) ∈ MblFn)
119106, 109, 118sylancl 586 . . 3 ((πœ‘ ∧ 𝐡 = 0) β†’ (𝐴 Γ— {0}) ∈ MblFn)
120117, 119eqeltrd 2833 . 2 ((πœ‘ ∧ 𝐡 = 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
12113adantr 481 . . 3 ((πœ‘ ∧ 0 < 𝐡) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
12211adantr 481 . . 3 ((πœ‘ ∧ 0 < 𝐡) β†’ 𝐴 ∈ dom vol)
123 simprl 769 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ)
124123rexrd 11260 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ*)
125124, 18syl 17 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
12620ad2ant2rl 747 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
127126biantrurd 533 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
12823ad2ant2rl 747 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ ℝ)
129128biantrurd 533 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
130 eqidd 2733 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
13111, 3, 66, 130ofc1 7692 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
132131ad2ant2rl 747 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
133132breq2d 5159 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
1343ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ)
135 simplr 767 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 0 < 𝐡)
136 ltdivmul 12085 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ (πΉβ€˜π‘§) ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 0 < 𝐡)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
137123, 128, 134, 135, 136syl112anc 1374 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
138133, 137bitr4d 281 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
139134, 135elrpd 13009 . . . . . . . . . . . . 13 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ+)
140123, 139rerpdivcld 13043 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ)
141140rexrd 11260 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ*)
142141, 89syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
143129, 138, 1423bitr4d 310 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
144125, 127, 1433bitr2d 306 . . . . . . . 8 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
145144anassrs 468 . . . . . . 7 ((((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
146145pm5.32da 579 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
14762ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
148147, 64syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
14966ad2antrr 724 . . . . . . 7 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ 𝐹 Fn 𝐴)
150149, 97syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
151146, 148, 1503bitr4d 310 . . . . 5 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞))))
152151eqrdv 2730 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) = (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)))
153102ad2antrr 724 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
154152, 153eqeltrd 2833 . . 3 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ∈ dom vol)
155124, 76syl 17 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
156126biantrurd 533 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
157 ltmuldiv2 12084 . . . . . . . . . . 11 (((πΉβ€˜π‘§) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 0 < 𝐡)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
158128, 123, 134, 135, 157syl112anc 1374 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
159132breq1d 5157 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
160141, 56syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
161128, 160mpbirand 705 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
162158, 159, 1613bitr4d 310 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
163155, 156, 1623bitr2d 306 . . . . . . . 8 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
164163anassrs 468 . . . . . . 7 ((((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
165164pm5.32da 579 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
166147, 95syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
167149, 68syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
168165, 166, 1673bitr4d 310 . . . . 5 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ 𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡)))))
169168eqrdv 2730 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) = (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))))
17073ad2antrr 724 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
171169, 170eqeltrd 2833 . . 3 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ∈ dom vol)
172121, 122, 154, 171ismbf2d 25148 . 2 ((πœ‘ ∧ 0 < 𝐡) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
173 0re 11212 . . 3 0 ∈ ℝ
174 lttri4 11294 . . 3 ((𝐡 ∈ ℝ ∧ 0 ∈ ℝ) β†’ (𝐡 < 0 ∨ 𝐡 = 0 ∨ 0 < 𝐡))
1753, 173, 174sylancl 586 . 2 (πœ‘ β†’ (𝐡 < 0 ∨ 𝐡 = 0 ∨ 0 < 𝐡))
176105, 120, 172, 175mpjao3dan 1431 1 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1086   = wceq 1541   ∈ wcel 2106  {csn 4627   class class class wbr 5147   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675   β€œ cima 5678   Fn wfn 6535  βŸΆwf 6536  β€˜cfv 6540  (class class class)co 7405   ∘f cof 7664  β„‚cc 11104  β„cr 11105  0cc0 11106   Β· cmul 11111  +∞cpnf 11241  -∞cmnf 11242  β„*cxr 11243   < clt 11244  -cneg 11441   / cdiv 11867  (,)cioo 13320  volcvol 24971  MblFncmbf 25122
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8699  df-map 8818  df-pm 8819  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-inf 9434  df-oi 9501  df-dju 9892  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-n0 12469  df-z 12555  df-uz 12819  df-q 12929  df-rp 12971  df-xadd 13089  df-ioo 13324  df-ico 13326  df-icc 13327  df-fz 13481  df-fzo 13624  df-fl 13753  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629  df-xmet 20929  df-met 20930  df-ovol 24972  df-vol 24973  df-mbf 25127
This theorem is referenced by:  mbfmulc2re  25156
  Copyright terms: Public domain W3C validator