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

Theorem mbfmulc2lem 23315
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 (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn)

Proof of Theorem mbfmulc2lem
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 remulcl 9966 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
21adantl 482 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
3 mbfmulc2re.2 . . . . . 6 (𝜑𝐵 ∈ ℝ)
4 fconst6g 6053 . . . . . 6 (𝐵 ∈ ℝ → (𝐴 × {𝐵}):𝐴⟶ℝ)
53, 4syl 17 . . . . 5 (𝜑 → (𝐴 × {𝐵}):𝐴⟶ℝ)
6 mbfmulc2lem.3 . . . . 5 (𝜑𝐹:𝐴⟶ℝ)
7 fdm 6010 . . . . . . 7 (𝐹:𝐴⟶ℝ → dom 𝐹 = 𝐴)
86, 7syl 17 . . . . . 6 (𝜑 → dom 𝐹 = 𝐴)
9 mbfmulc2re.1 . . . . . . 7 (𝜑𝐹 ∈ MblFn)
10 mbfdm 23296 . . . . . . 7 (𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol)
119, 10syl 17 . . . . . 6 (𝜑 → dom 𝐹 ∈ dom vol)
128, 11eqeltrrd 2705 . . . . 5 (𝜑𝐴 ∈ dom vol)
13 inidm 3805 . . . . 5 (𝐴𝐴) = 𝐴
142, 5, 6, 12, 12, 13off 6866 . . . 4 (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹):𝐴⟶ℝ)
1514adantr 481 . . 3 ((𝜑𝐵 < 0) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹):𝐴⟶ℝ)
1612adantr 481 . . 3 ((𝜑𝐵 < 0) → 𝐴 ∈ dom vol)
17 simprl 793 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑦 ∈ ℝ)
1817rexrd 10034 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑦 ∈ ℝ*)
19 elioopnf 12206 . . . . . . . . . 10 (𝑦 ∈ ℝ* → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧))))
2018, 19syl 17 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧))))
2114ffvelrnda 6316 . . . . . . . . . . 11 ((𝜑𝑧𝐴) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ)
2221ad2ant2rl 784 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ)
2322biantrurd 529 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧))))
246ffvelrnda 6316 . . . . . . . . . . . 12 ((𝜑𝑧𝐴) → (𝐹𝑧) ∈ ℝ)
2524ad2ant2rl 784 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝐹𝑧) ∈ ℝ)
2625biantrurd 529 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) < (𝑦 / 𝐵) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < (𝑦 / 𝐵))))
27 simprr 795 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑧𝐴)
2812ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐴 ∈ dom vol)
293ad2antrr 761 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 ∈ ℝ)
306ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐹:𝐴⟶ℝ)
31 ffn 6004 . . . . . . . . . . . . . . 15 (𝐹:𝐴⟶ℝ → 𝐹 Fn 𝐴)
3230, 31syl 17 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐹 Fn 𝐴)
33 eqidd 2627 . . . . . . . . . . . . . 14 ((((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) ∧ 𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
3428, 29, 32, 33ofc1 6874 . . . . . . . . . . . . 13 ((((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) ∧ 𝑧𝐴) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) = (𝐵 · (𝐹𝑧)))
3527, 34mpdan 701 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) = (𝐵 · (𝐹𝑧)))
3635breq2d 4630 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹𝑧))))
3717renegcld 10402 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → -𝑦 ∈ ℝ)
3829renegcld 10402 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → -𝐵 ∈ ℝ)
39 simplr 791 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 < 0)
4029lt0neg1d 10542 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝐵 < 0 ↔ 0 < -𝐵))
4139, 40mpbid 222 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 0 < -𝐵)
42 ltmuldiv2 10842 . . . . . . . . . . . . 13 (((𝐹𝑧) ∈ ℝ ∧ -𝑦 ∈ ℝ ∧ (-𝐵 ∈ ℝ ∧ 0 < -𝐵)) → ((-𝐵 · (𝐹𝑧)) < -𝑦 ↔ (𝐹𝑧) < (-𝑦 / -𝐵)))
4325, 37, 38, 41, 42syl112anc 1327 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((-𝐵 · (𝐹𝑧)) < -𝑦 ↔ (𝐹𝑧) < (-𝑦 / -𝐵)))
4429recnd 10013 . . . . . . . . . . . . . . 15 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 ∈ ℂ)
4525recnd 10013 . . . . . . . . . . . . . . 15 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝐹𝑧) ∈ ℂ)
4644, 45mulneg1d 10428 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (-𝐵 · (𝐹𝑧)) = -(𝐵 · (𝐹𝑧)))
4746breq1d 4628 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((-𝐵 · (𝐹𝑧)) < -𝑦 ↔ -(𝐵 · (𝐹𝑧)) < -𝑦))
4835, 22eqeltrrd 2705 . . . . . . . . . . . . . 14 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝐵 · (𝐹𝑧)) ∈ ℝ)
4917, 48ltnegd 10550 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (𝐵 · (𝐹𝑧)) ↔ -(𝐵 · (𝐹𝑧)) < -𝑦))
5047, 49bitr4d 271 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((-𝐵 · (𝐹𝑧)) < -𝑦𝑦 < (𝐵 · (𝐹𝑧))))
5143, 50bitr3d 270 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) < (-𝑦 / -𝐵) ↔ 𝑦 < (𝐵 · (𝐹𝑧))))
5217recnd 10013 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑦 ∈ ℂ)
5339lt0ne0d 10538 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 ≠ 0)
5452, 44, 53div2negd 10761 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (-𝑦 / -𝐵) = (𝑦 / 𝐵))
5554breq2d 4630 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) < (-𝑦 / -𝐵) ↔ (𝐹𝑧) < (𝑦 / 𝐵)))
5636, 51, 553bitr2d 296 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ (𝐹𝑧) < (𝑦 / 𝐵)))
5717, 29, 53redivcld 10798 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 / 𝐵) ∈ ℝ)
5857rexrd 10034 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 / 𝐵) ∈ ℝ*)
59 elioomnf 12207 . . . . . . . . . . 11 ((𝑦 / 𝐵) ∈ ℝ* → ((𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < (𝑦 / 𝐵))))
6058, 59syl 17 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < (𝑦 / 𝐵))))
6126, 56, 603bitr4d 300 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
6220, 23, 613bitr2d 296 . . . . . . . 8 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
6362anassrs 679 . . . . . . 7 ((((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
6463pm5.32da 672 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))))
65 ffn 6004 . . . . . . . . 9 (((𝐴 × {𝐵}) ∘𝑓 · 𝐹):𝐴⟶ℝ → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴)
6614, 65syl 17 . . . . . . . 8 (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴)
6766ad2antrr 761 . . . . . . 7 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴)
68 elpreima 6294 . . . . . . 7 (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴 → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞))))
6967, 68syl 17 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞))))
706, 31syl 17 . . . . . . . 8 (𝜑𝐹 Fn 𝐴)
7170ad2antrr 761 . . . . . . 7 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn 𝐴)
72 elpreima 6294 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))))
7371, 72syl 17 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))))
7464, 69, 733bitr4d 300 . . . . 5 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ↔ 𝑧 ∈ (𝐹 “ (-∞(,)(𝑦 / 𝐵)))))
7574eqrdv 2624 . . . 4 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) = (𝐹 “ (-∞(,)(𝑦 / 𝐵))))
76 mbfima 23300 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol)
779, 6, 76syl2anc 692 . . . . 5 (𝜑 → (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol)
7877ad2antrr 761 . . . 4 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol)
7975, 78eqeltrd 2704 . . 3 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ∈ dom vol)
80 elioomnf 12207 . . . . . . . . . 10 (𝑦 ∈ ℝ* → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦)))
8118, 80syl 17 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦)))
8222biantrurd 529 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦)))
8325biantrurd 529 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹𝑧))))
8435breq1d 4628 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ (𝐵 · (𝐹𝑧)) < 𝑦))
8546breq2d 4630 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (-𝑦 < (-𝐵 · (𝐹𝑧)) ↔ -𝑦 < -(𝐵 · (𝐹𝑧))))
8654breq1d 4628 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((-𝑦 / -𝐵) < (𝐹𝑧) ↔ (𝑦 / 𝐵) < (𝐹𝑧)))
87 ltdivmul 10843 . . . . . . . . . . . . . 14 ((-𝑦 ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ ∧ (-𝐵 ∈ ℝ ∧ 0 < -𝐵)) → ((-𝑦 / -𝐵) < (𝐹𝑧) ↔ -𝑦 < (-𝐵 · (𝐹𝑧))))
8837, 25, 38, 41, 87syl112anc 1327 . . . . . . . . . . . . 13 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((-𝑦 / -𝐵) < (𝐹𝑧) ↔ -𝑦 < (-𝐵 · (𝐹𝑧))))
8986, 88bitr3d 270 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ -𝑦 < (-𝐵 · (𝐹𝑧))))
9048, 17ltnegd 10550 . . . . . . . . . . . 12 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐵 · (𝐹𝑧)) < 𝑦 ↔ -𝑦 < -(𝐵 · (𝐹𝑧))))
9185, 89, 903bitr4d 300 . . . . . . . . . . 11 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ (𝐵 · (𝐹𝑧)) < 𝑦))
9284, 91bitr4d 271 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ (𝑦 / 𝐵) < (𝐹𝑧)))
93 elioopnf 12206 . . . . . . . . . . 11 ((𝑦 / 𝐵) ∈ ℝ* → ((𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹𝑧))))
9458, 93syl 17 . . . . . . . . . 10 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹𝑧))))
9583, 92, 943bitr4d 300 . . . . . . . . 9 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
9681, 82, 953bitr2d 296 . . . . . . . 8 (((𝜑𝐵 < 0) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
9796anassrs 679 . . . . . . 7 ((((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) ∧ 𝑧𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
9897pm5.32da 672 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → ((𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))))
99 elpreima 6294 . . . . . . 7 (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴 → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦))))
10067, 99syl 17 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦))))
101 elpreima 6294 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑧 ∈ (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))))
10271, 101syl 17 . . . . . 6 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))))
10398, 100, 1023bitr4d 300 . . . . 5 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ↔ 𝑧 ∈ (𝐹 “ ((𝑦 / 𝐵)(,)+∞))))
104103eqrdv 2624 . . . 4 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) = (𝐹 “ ((𝑦 / 𝐵)(,)+∞)))
105 mbfima 23300 . . . . . 6 ((𝐹 ∈ MblFn ∧ 𝐹:𝐴⟶ℝ) → (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom vol)
1069, 6, 105syl2anc 692 . . . . 5 (𝜑 → (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom vol)
107106ad2antrr 761 . . . 4 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom vol)
108104, 107eqeltrd 2704 . . 3 (((𝜑𝐵 < 0) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ∈ dom vol)
10915, 16, 79, 108ismbf2d 23309 . 2 ((𝜑𝐵 < 0) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn)
11012adantr 481 . . . 4 ((𝜑𝐵 = 0) → 𝐴 ∈ dom vol)
1116adantr 481 . . . 4 ((𝜑𝐵 = 0) → 𝐹:𝐴⟶ℝ)
112 simpr 477 . . . . 5 ((𝜑𝐵 = 0) → 𝐵 = 0)
113 0cn 9977 . . . . 5 0 ∈ ℂ
114112, 113syl6eqel 2712 . . . 4 ((𝜑𝐵 = 0) → 𝐵 ∈ ℂ)
115 0cnd 9978 . . . 4 ((𝜑𝐵 = 0) → 0 ∈ ℂ)
116 simplr 791 . . . . . 6 (((𝜑𝐵 = 0) ∧ 𝑥 ∈ ℝ) → 𝐵 = 0)
117116oveq1d 6620 . . . . 5 (((𝜑𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (𝐵 · 𝑥) = (0 · 𝑥))
118 mul02lem2 10158 . . . . . 6 (𝑥 ∈ ℝ → (0 · 𝑥) = 0)
119118adantl 482 . . . . 5 (((𝜑𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (0 · 𝑥) = 0)
120117, 119eqtrd 2660 . . . 4 (((𝜑𝐵 = 0) ∧ 𝑥 ∈ ℝ) → (𝐵 · 𝑥) = 0)
121110, 111, 114, 115, 120caofid2 6882 . . 3 ((𝜑𝐵 = 0) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) = (𝐴 × {0}))
122 mbfconst 23303 . . . 4 ((𝐴 ∈ dom vol ∧ 0 ∈ ℂ) → (𝐴 × {0}) ∈ MblFn)
123110, 113, 122sylancl 693 . . 3 ((𝜑𝐵 = 0) → (𝐴 × {0}) ∈ MblFn)
124121, 123eqeltrd 2704 . 2 ((𝜑𝐵 = 0) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn)
12514adantr 481 . . 3 ((𝜑 ∧ 0 < 𝐵) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹):𝐴⟶ℝ)
12612adantr 481 . . 3 ((𝜑 ∧ 0 < 𝐵) → 𝐴 ∈ dom vol)
127 simprl 793 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑦 ∈ ℝ)
128127rexrd 10034 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝑦 ∈ ℝ*)
129128, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧))))
13021ad2ant2rl 784 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ)
131130biantrurd 529 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ 𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧))))
13224ad2ant2rl 784 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝐹𝑧) ∈ ℝ)
133132biantrurd 529 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹𝑧))))
134 eqidd 2627 . . . . . . . . . . . . . 14 ((𝜑𝑧𝐴) → (𝐹𝑧) = (𝐹𝑧))
13512, 3, 70, 134ofc1 6874 . . . . . . . . . . . . 13 ((𝜑𝑧𝐴) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) = (𝐵 · (𝐹𝑧)))
136135ad2ant2rl 784 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) = (𝐵 · (𝐹𝑧)))
137136breq2d 4630 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ 𝑦 < (𝐵 · (𝐹𝑧))))
1383ad2antrr 761 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 ∈ ℝ)
139 simplr 791 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 0 < 𝐵)
140 ltdivmul 10843 . . . . . . . . . . . 12 ((𝑦 ∈ ℝ ∧ (𝐹𝑧) ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ 𝑦 < (𝐵 · (𝐹𝑧))))
141127, 132, 138, 139, 140syl112anc 1327 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝑦 / 𝐵) < (𝐹𝑧) ↔ 𝑦 < (𝐵 · (𝐹𝑧))))
142137, 141bitr4d 271 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ (𝑦 / 𝐵) < (𝐹𝑧)))
143138, 139elrpd 11813 . . . . . . . . . . . . 13 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → 𝐵 ∈ ℝ+)
144127, 143rerpdivcld 11847 . . . . . . . . . . . 12 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 / 𝐵) ∈ ℝ)
145144rexrd 10034 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 / 𝐵) ∈ ℝ*)
146145, 93syl 17 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝑦 / 𝐵) < (𝐹𝑧))))
147133, 142, 1463bitr4d 300 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → (𝑦 < (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
148129, 131, 1473bitr2d 296 . . . . . . . 8 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
149148anassrs 679 . . . . . . 7 ((((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝑧𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞) ↔ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞)))
150149pm5.32da 672 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))))
15166ad2antrr 761 . . . . . . 7 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) Fn 𝐴)
152151, 68syl 17 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (𝑦(,)+∞))))
15370ad2antrr 761 . . . . . . 7 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → 𝐹 Fn 𝐴)
154153, 101syl 17 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ ((𝑦 / 𝐵)(,)+∞))))
155150, 152, 1543bitr4d 300 . . . . 5 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ↔ 𝑧 ∈ (𝐹 “ ((𝑦 / 𝐵)(,)+∞))))
156155eqrdv 2624 . . . 4 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) = (𝐹 “ ((𝑦 / 𝐵)(,)+∞)))
157106ad2antrr 761 . . . 4 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐹 “ ((𝑦 / 𝐵)(,)+∞)) ∈ dom vol)
158156, 157eqeltrd 2704 . . 3 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (𝑦(,)+∞)) ∈ dom vol)
159128, 80syl 17 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦)))
160130biantrurd 529 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ ℝ ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦)))
161 ltmuldiv2 10842 . . . . . . . . . . 11 (((𝐹𝑧) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 0 < 𝐵)) → ((𝐵 · (𝐹𝑧)) < 𝑦 ↔ (𝐹𝑧) < (𝑦 / 𝐵)))
162132, 127, 138, 139, 161syl112anc 1327 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐵 · (𝐹𝑧)) < 𝑦 ↔ (𝐹𝑧) < (𝑦 / 𝐵)))
163136breq1d 4628 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ (𝐵 · (𝐹𝑧)) < 𝑦))
164145, 59syl 17 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < (𝑦 / 𝐵))))
165132biantrurd 529 . . . . . . . . . . 11 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) < (𝑦 / 𝐵) ↔ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝑧) < (𝑦 / 𝐵))))
166164, 165bitr4d 271 . . . . . . . . . 10 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)) ↔ (𝐹𝑧) < (𝑦 / 𝐵)))
167162, 163, 1663bitr4d 300 . . . . . . . . 9 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) < 𝑦 ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
168159, 160, 1673bitr2d 296 . . . . . . . 8 (((𝜑 ∧ 0 < 𝐵) ∧ (𝑦 ∈ ℝ ∧ 𝑧𝐴)) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
169168anassrs 679 . . . . . . 7 ((((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) ∧ 𝑧𝐴) → ((((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦) ↔ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵))))
170169pm5.32da 672 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → ((𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))))
171151, 99syl 17 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ↔ (𝑧𝐴 ∧ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹)‘𝑧) ∈ (-∞(,)𝑦))))
172153, 72syl 17 . . . . . 6 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ↔ (𝑧𝐴 ∧ (𝐹𝑧) ∈ (-∞(,)(𝑦 / 𝐵)))))
173170, 171, 1723bitr4d 300 . . . . 5 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝑧 ∈ (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ↔ 𝑧 ∈ (𝐹 “ (-∞(,)(𝑦 / 𝐵)))))
174173eqrdv 2624 . . . 4 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) = (𝐹 “ (-∞(,)(𝑦 / 𝐵))))
17577ad2antrr 761 . . . 4 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (𝐹 “ (-∞(,)(𝑦 / 𝐵))) ∈ dom vol)
176174, 175eqeltrd 2704 . . 3 (((𝜑 ∧ 0 < 𝐵) ∧ 𝑦 ∈ ℝ) → (((𝐴 × {𝐵}) ∘𝑓 · 𝐹) “ (-∞(,)𝑦)) ∈ dom vol)
177125, 126, 158, 176ismbf2d 23309 . 2 ((𝜑 ∧ 0 < 𝐵) → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn)
178 0re 9985 . . 3 0 ∈ ℝ
179 lttri4 10067 . . 3 ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → (𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵))
1803, 178, 179sylancl 693 . 2 (𝜑 → (𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵))
181109, 124, 177, 180mpjao3dan 1392 1 (𝜑 → ((𝐴 × {𝐵}) ∘𝑓 · 𝐹) ∈ MblFn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3o 1035   = wceq 1480  wcel 1992  {csn 4153   class class class wbr 4618   × cxp 5077  ccnv 5078  dom cdm 5079  cima 5082   Fn wfn 5845  wf 5846  cfv 5850  (class class class)co 6605  𝑓 cof 6849  cc 9879  cr 9880  0cc0 9881   · cmul 9886  +∞cpnf 10016  -∞cmnf 10017  *cxr 10018   < clt 10019  -cneg 10212   / cdiv 10629  (,)cioo 12114  volcvol 23134  MblFncmbf 23284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-inf2 8483  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-isom 5859  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-of 6851  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-2o 7507  df-oadd 7510  df-er 7688  df-map 7805  df-pm 7806  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-sup 8293  df-inf 8294  df-oi 8360  df-card 8710  df-cda 8935  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-nn 10966  df-2 11024  df-3 11025  df-n0 11238  df-z 11323  df-uz 11632  df-q 11733  df-rp 11777  df-xadd 11891  df-ioo 12118  df-ico 12120  df-icc 12121  df-fz 12266  df-fzo 12404  df-fl 12530  df-seq 12739  df-exp 12798  df-hash 13055  df-cj 13768  df-re 13769  df-im 13770  df-sqrt 13904  df-abs 13905  df-clim 14148  df-sum 14346  df-xmet 19653  df-met 19654  df-ovol 23135  df-vol 23136  df-mbf 23289
This theorem is referenced by:  mbfmulc2re  23316
  Copyright terms: Public domain W3C validator