MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mbfmulc2lem Structured version   Visualization version   GIF version

Theorem mbfmulc2lem 25027
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 11143 . . . . . 6 ((π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
21adantl 483 . . . . 5 ((πœ‘ ∧ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)) β†’ (π‘₯ Β· 𝑦) ∈ ℝ)
3 mbfmulc2re.2 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ ℝ)
4 fconst6g 6736 . . . . . 6 (𝐡 ∈ ℝ β†’ (𝐴 Γ— {𝐡}):π΄βŸΆβ„)
53, 4syl 17 . . . . 5 (πœ‘ β†’ (𝐴 Γ— {𝐡}):π΄βŸΆβ„)
6 mbfmulc2lem.3 . . . . 5 (πœ‘ β†’ 𝐹:π΄βŸΆβ„)
76fdmd 6684 . . . . . 6 (πœ‘ β†’ dom 𝐹 = 𝐴)
8 mbfmulc2re.1 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ MblFn)
9 mbfdm 25006 . . . . . . 7 (𝐹 ∈ MblFn β†’ dom 𝐹 ∈ dom vol)
108, 9syl 17 . . . . . 6 (πœ‘ β†’ dom 𝐹 ∈ dom vol)
117, 10eqeltrrd 2839 . . . . 5 (πœ‘ β†’ 𝐴 ∈ dom vol)
12 inidm 4183 . . . . 5 (𝐴 ∩ 𝐴) = 𝐴
132, 5, 6, 11, 11, 12off 7640 . . . 4 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
1413adantr 482 . . 3 ((πœ‘ ∧ 𝐡 < 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
1511adantr 482 . . 3 ((πœ‘ ∧ 𝐡 < 0) β†’ 𝐴 ∈ dom vol)
16 simprl 770 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ)
1716rexrd 11212 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ*)
18 elioopnf 13367 . . . . . . . . . 10 (𝑦 ∈ ℝ* β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
1917, 18syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
2013ffvelcdmda 7040 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
2120ad2ant2rl 748 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
2221biantrurd 534 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
236ffvelcdmda 7040 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) ∈ ℝ)
2423ad2ant2rl 748 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ ℝ)
2524biantrurd 534 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (𝑦 / 𝐡) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
26 simprr 772 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑧 ∈ 𝐴)
2711ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐴 ∈ dom vol)
283ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ)
296ad2antrr 725 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐹:π΄βŸΆβ„)
3029ffnd 6674 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐹 Fn 𝐴)
31 eqidd 2738 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
3227, 28, 30, 31ofc1 7648 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
3326, 32mpdan 686 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
3433breq2d 5122 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
3533, 21eqeltrrd 2839 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝐡 Β· (πΉβ€˜π‘§)) ∈ ℝ)
3616, 35ltnegd 11740 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (𝐡 Β· (πΉβ€˜π‘§)) ↔ -(𝐡 Β· (πΉβ€˜π‘§)) < -𝑦))
3728recnd 11190 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ β„‚)
3824recnd 11190 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ β„‚)
3937, 38mulneg1d 11615 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝐡 Β· (πΉβ€˜π‘§)) = -(𝐡 Β· (πΉβ€˜π‘§)))
4039breq1d 5120 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ -(𝐡 Β· (πΉβ€˜π‘§)) < -𝑦))
4116renegcld 11589 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ -𝑦 ∈ ℝ)
4228renegcld 11589 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ -𝐡 ∈ ℝ)
43 simplr 768 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 < 0)
4428lt0neg1d 11731 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝐡 < 0 ↔ 0 < -𝐡))
4543, 44mpbid 231 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 0 < -𝐡)
46 ltmuldiv2 12036 . . . . . . . . . . . . 13 (((πΉβ€˜π‘§) ∈ ℝ ∧ -𝑦 ∈ ℝ ∧ (-𝐡 ∈ ℝ ∧ 0 < -𝐡)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ (πΉβ€˜π‘§) < (-𝑦 / -𝐡)))
4724, 41, 42, 45, 46syl112anc 1375 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝐡 Β· (πΉβ€˜π‘§)) < -𝑦 ↔ (πΉβ€˜π‘§) < (-𝑦 / -𝐡)))
4836, 40, 473bitr2rd 308 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (-𝑦 / -𝐡) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
4916recnd 11190 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ β„‚)
5043lt0ne0d 11727 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 β‰  0)
5149, 37, 50div2negd 11953 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝑦 / -𝐡) = (𝑦 / 𝐡))
5251breq2d 5122 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) < (-𝑦 / -𝐡) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
5334, 48, 523bitr2d 307 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
5416, 28, 50redivcld 11990 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ)
5554rexrd 11212 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ*)
56 elioomnf 13368 . . . . . . . . . . 11 ((𝑦 / 𝐡) ∈ ℝ* β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
5755, 56syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
5825, 53, 573bitr4d 311 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
5919, 22, 583bitr2d 307 . . . . . . . 8 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
6059anassrs 469 . . . . . . 7 ((((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
6160pm5.32da 580 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
6213ffnd 6674 . . . . . . . 8 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
6362ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
64 elpreima 7013 . . . . . . 7 (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴 β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
6563, 64syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
666ffnd 6674 . . . . . . . 8 (πœ‘ β†’ 𝐹 Fn 𝐴)
6766ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ 𝐹 Fn 𝐴)
68 elpreima 7013 . . . . . . 7 (𝐹 Fn 𝐴 β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
6967, 68syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
7061, 65, 693bitr4d 311 . . . . 5 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡)))))
7170eqrdv 2735 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) = (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))))
72 mbfima 25010 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:π΄βŸΆβ„) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
738, 6, 72syl2anc 585 . . . . 5 (πœ‘ β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
7473ad2antrr 725 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
7571, 74eqeltrd 2838 . . 3 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ∈ dom vol)
76 elioomnf 13368 . . . . . . . . . 10 (𝑦 ∈ ℝ* β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7717, 76syl 17 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7821biantrurd 534 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
7924biantrurd 534 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
8033breq1d 5120 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
8139breq2d 5122 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (-𝑦 < (-𝐡 Β· (πΉβ€˜π‘§)) ↔ -𝑦 < -(𝐡 Β· (πΉβ€˜π‘§))))
8251breq1d 5120 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
83 ltdivmul 12037 . . . . . . . . . . . . . 14 ((-𝑦 ∈ ℝ ∧ (πΉβ€˜π‘§) ∈ ℝ ∧ (-𝐡 ∈ ℝ ∧ 0 < -𝐡)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8441, 24, 42, 45, 83syl112anc 1375 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((-𝑦 / -𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8582, 84bitr3d 281 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ -𝑦 < (-𝐡 Β· (πΉβ€˜π‘§))))
8635, 16ltnegd 11740 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ -𝑦 < -(𝐡 Β· (πΉβ€˜π‘§))))
8781, 85, 863bitr4d 311 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
8880, 87bitr4d 282 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
89 elioopnf 13367 . . . . . . . . . . 11 ((𝑦 / 𝐡) ∈ ℝ* β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
9055, 89syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
9179, 88, 903bitr4d 311 . . . . . . . . 9 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9277, 78, 913bitr2d 307 . . . . . . . 8 (((πœ‘ ∧ 𝐡 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9392anassrs 469 . . . . . . 7 ((((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
9493pm5.32da 580 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
95 elpreima 7013 . . . . . . 7 (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴 β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
9663, 95syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
97 elpreima 7013 . . . . . . 7 (𝐹 Fn 𝐴 β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
9867, 97syl 17 . . . . . 6 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
9994, 96, 983bitr4d 311 . . . . 5 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ 𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞))))
10099eqrdv 2735 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) = (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)))
101 mbfima 25010 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:π΄βŸΆβ„) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
1028, 6, 101syl2anc 585 . . . . 5 (πœ‘ β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
103102ad2antrr 725 . . . 4 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
104100, 103eqeltrd 2838 . . 3 (((πœ‘ ∧ 𝐡 < 0) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ∈ dom vol)
10514, 15, 75, 104ismbf2d 25020 . 2 ((πœ‘ ∧ 𝐡 < 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
10611adantr 482 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐴 ∈ dom vol)
1076adantr 482 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐹:π΄βŸΆβ„)
108 simpr 486 . . . . 5 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐡 = 0)
109 0cn 11154 . . . . 5 0 ∈ β„‚
110108, 109eqeltrdi 2846 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 𝐡 ∈ β„‚)
111 0cnd 11155 . . . 4 ((πœ‘ ∧ 𝐡 = 0) β†’ 0 ∈ β„‚)
112 simplr 768 . . . . . 6 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ 𝐡 = 0)
113112oveq1d 7377 . . . . 5 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (𝐡 Β· π‘₯) = (0 Β· π‘₯))
114 mul02lem2 11339 . . . . . 6 (π‘₯ ∈ ℝ β†’ (0 Β· π‘₯) = 0)
115114adantl 483 . . . . 5 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (0 Β· π‘₯) = 0)
116113, 115eqtrd 2777 . . . 4 (((πœ‘ ∧ 𝐡 = 0) ∧ π‘₯ ∈ ℝ) β†’ (𝐡 Β· π‘₯) = 0)
117106, 107, 110, 111, 116caofid2 7656 . . 3 ((πœ‘ ∧ 𝐡 = 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) = (𝐴 Γ— {0}))
118 mbfconst 25013 . . . 4 ((𝐴 ∈ dom vol ∧ 0 ∈ β„‚) β†’ (𝐴 Γ— {0}) ∈ MblFn)
119106, 109, 118sylancl 587 . . 3 ((πœ‘ ∧ 𝐡 = 0) β†’ (𝐴 Γ— {0}) ∈ MblFn)
120117, 119eqeltrd 2838 . 2 ((πœ‘ ∧ 𝐡 = 0) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
12113adantr 482 . . 3 ((πœ‘ ∧ 0 < 𝐡) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹):π΄βŸΆβ„)
12211adantr 482 . . 3 ((πœ‘ ∧ 0 < 𝐡) β†’ 𝐴 ∈ dom vol)
123 simprl 770 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ)
124123rexrd 11212 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝑦 ∈ ℝ*)
125124, 18syl 17 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
12620ad2ant2rl 748 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ)
127126biantrurd 534 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ 𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§))))
12823ad2ant2rl 748 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (πΉβ€˜π‘§) ∈ ℝ)
129128biantrurd 534 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
130 eqidd 2738 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (πΉβ€˜π‘§) = (πΉβ€˜π‘§))
13111, 3, 66, 130ofc1 7648 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝐴) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
132131ad2ant2rl 748 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) = (𝐡 Β· (πΉβ€˜π‘§)))
133132breq2d 5122 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
1343ad2antrr 725 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ)
135 simplr 768 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 0 < 𝐡)
136 ltdivmul 12037 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ (πΉβ€˜π‘§) ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 0 < 𝐡)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
137123, 128, 134, 135, 136syl112anc 1375 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝑦 / 𝐡) < (πΉβ€˜π‘§) ↔ 𝑦 < (𝐡 Β· (πΉβ€˜π‘§))))
138133, 137bitr4d 282 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (𝑦 / 𝐡) < (πΉβ€˜π‘§)))
139134, 135elrpd 12961 . . . . . . . . . . . . 13 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ 𝐡 ∈ ℝ+)
140123, 139rerpdivcld 12995 . . . . . . . . . . . 12 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ)
141140rexrd 11212 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 / 𝐡) ∈ ℝ*)
142141, 89syl 17 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (𝑦 / 𝐡) < (πΉβ€˜π‘§))))
143129, 138, 1423bitr4d 311 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ (𝑦 < (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
144125, 127, 1433bitr2d 307 . . . . . . . 8 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
145144anassrs 469 . . . . . . 7 ((((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞) ↔ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞)))
146145pm5.32da 580 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
14762ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) Fn 𝐴)
148147, 64syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (𝑦(,)+∞))))
14966ad2antrr 725 . . . . . . 7 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ 𝐹 Fn 𝐴)
150149, 97syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ ((𝑦 / 𝐡)(,)+∞))))
151146, 148, 1503bitr4d 311 . . . . 5 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ↔ 𝑧 ∈ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞))))
152151eqrdv 2735 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) = (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)))
153102ad2antrr 725 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ ((𝑦 / 𝐡)(,)+∞)) ∈ dom vol)
154152, 153eqeltrd 2838 . . 3 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (𝑦(,)+∞)) ∈ dom vol)
155124, 76syl 17 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
156126biantrurd 534 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ ℝ ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦)))
157 ltmuldiv2 12036 . . . . . . . . . . 11 (((πΉβ€˜π‘§) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐡 ∈ ℝ ∧ 0 < 𝐡)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
158128, 123, 134, 135, 157syl112anc 1375 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((𝐡 Β· (πΉβ€˜π‘§)) < 𝑦 ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
159132breq1d 5120 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (𝐡 Β· (πΉβ€˜π‘§)) < 𝑦))
160141, 56syl 17 . . . . . . . . . . 11 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ ((πΉβ€˜π‘§) ∈ ℝ ∧ (πΉβ€˜π‘§) < (𝑦 / 𝐡))))
161128, 160mpbirand 706 . . . . . . . . . 10 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)) ↔ (πΉβ€˜π‘§) < (𝑦 / 𝐡)))
162158, 159, 1613bitr4d 311 . . . . . . . . 9 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) < 𝑦 ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
163155, 156, 1623bitr2d 307 . . . . . . . 8 (((πœ‘ ∧ 0 < 𝐡) ∧ (𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴)) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
164163anassrs 469 . . . . . . 7 ((((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) ∧ 𝑧 ∈ 𝐴) β†’ ((((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦) ↔ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡))))
165164pm5.32da 580 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ ((𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
166147, 95syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ (𝑧 ∈ 𝐴 ∧ (((𝐴 Γ— {𝐡}) ∘f Β· 𝐹)β€˜π‘§) ∈ (-∞(,)𝑦))))
167149, 68syl 17 . . . . . 6 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ↔ (𝑧 ∈ 𝐴 ∧ (πΉβ€˜π‘§) ∈ (-∞(,)(𝑦 / 𝐡)))))
168165, 166, 1673bitr4d 311 . . . . 5 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (𝑧 ∈ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ↔ 𝑧 ∈ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡)))))
169168eqrdv 2735 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) = (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))))
17073ad2antrr 725 . . . 4 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (◑𝐹 β€œ (-∞(,)(𝑦 / 𝐡))) ∈ dom vol)
171169, 170eqeltrd 2838 . . 3 (((πœ‘ ∧ 0 < 𝐡) ∧ 𝑦 ∈ ℝ) β†’ (β—‘((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) β€œ (-∞(,)𝑦)) ∈ dom vol)
172121, 122, 154, 171ismbf2d 25020 . 2 ((πœ‘ ∧ 0 < 𝐡) β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
173 0re 11164 . . 3 0 ∈ ℝ
174 lttri4 11246 . . 3 ((𝐡 ∈ ℝ ∧ 0 ∈ ℝ) β†’ (𝐡 < 0 ∨ 𝐡 = 0 ∨ 0 < 𝐡))
1753, 173, 174sylancl 587 . 2 (πœ‘ β†’ (𝐡 < 0 ∨ 𝐡 = 0 ∨ 0 < 𝐡))
176105, 120, 172, 175mpjao3dan 1432 1 (πœ‘ β†’ ((𝐴 Γ— {𝐡}) ∘f Β· 𝐹) ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ w3o 1087   = wceq 1542   ∈ wcel 2107  {csn 4591   class class class wbr 5110   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620  β„‚cc 11056  β„cr 11057  0cc0 11058   Β· cmul 11063  +∞cpnf 11193  -∞cmnf 11194  β„*cxr 11195   < clt 11196  -cneg 11393   / cdiv 11819  (,)cioo 13271  volcvol 24843  MblFncmbf 24994
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 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-z 12507  df-uz 12771  df-q 12881  df-rp 12923  df-xadd 13041  df-ioo 13275  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-sum 15578  df-xmet 20805  df-met 20806  df-ovol 24844  df-vol 24845  df-mbf 24999
This theorem is referenced by:  mbfmulc2re  25028
  Copyright terms: Public domain W3C validator