Metamath Proof Explorer

Theorem mbfmulc2lem

Description: Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfmulc2re.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfmulc2re.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
mbfmulc2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
Assertion mbfmulc2lem ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfmulc2re.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfmulc2re.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 mbfmulc2lem.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ )
4 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
5 4 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
6 fconst6g ⊢ ( 𝐵 ∈ ℝ → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ ℝ )
7 2 6 syl ⊢ ( 𝜑 → ( 𝐴 × { 𝐵 } ) : 𝐴 ⟶ ℝ )
8 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
9 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
10 1 9 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
11 8 10 eqeltrrd ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
12 inidm ⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
13 5 7 3 11 11 12 off ⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) : 𝐴 ⟶ ℝ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 0 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) : 𝐴 ⟶ ℝ )
15 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 < 0 ) → 𝐴 ∈ dom vol )
16 simprl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
17 16 rexrd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ* )
18 elioopnf ⊢ ( 𝑦 ∈ ℝ* → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ) ) )
19 17 18 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ) ) )
20 13 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
21 20 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
22 21 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ) ) )
23 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
24 23 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
25 24 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) ) )
26 simprr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
27 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐴 ∈ dom vol )
28 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
29 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐹 : 𝐴 ⟶ ℝ )
30 29 ffnd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐹 Fn 𝐴 )
31 eqidd ⊢ ( ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
32 27 28 30 31 ofc1 ⊢ ( ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) )
33 26 32 mpdan ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) )
34 33 breq2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
35 33 21 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ∈ ℝ )
36 16 35 ltnegd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ↔ - ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < - 𝑦 ) )
37 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 ∈ ℂ )
38 24 recnd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
39 37 38 mulneg1d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) = - ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) )
40 39 breq1d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < - 𝑦 ↔ - ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < - 𝑦 ) )
41 16 renegcld ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → - 𝑦 ∈ ℝ )
42 28 renegcld ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → - 𝐵 ∈ ℝ )
43 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 < 0 )
44 28 lt0neg1d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐵 < 0 ↔ 0 < - 𝐵 ) )
45 43 44 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 0 < - 𝐵 )
46 ltmuldiv2 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ - 𝑦 ∈ ℝ ∧ ( - 𝐵 ∈ ℝ ∧ 0 < - 𝐵 ) ) → ( ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < - 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) < ( - 𝑦 / - 𝐵 ) ) )
47 24 41 42 45 46 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < - 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) < ( - 𝑦 / - 𝐵 ) ) )
48 36 40 47 3bitr2rd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) < ( - 𝑦 / - 𝐵 ) ↔ 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
49 16 recnd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ ℂ )
50 43 lt0ne0d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 ≠ 0 )
51 49 37 50 div2negd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( - 𝑦 / - 𝐵 ) = ( 𝑦 / 𝐵 ) )
52 51 breq2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) < ( - 𝑦 / - 𝐵 ) ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) )
53 34 48 52 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) )
54 16 28 50 redivcld ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 / 𝐵 ) ∈ ℝ )
55 54 rexrd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 / 𝐵 ) ∈ ℝ* )
56 elioomnf ⊢ ( ( 𝑦 / 𝐵 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) ) )
57 55 56 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) ) )
58 25 53 57 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
59 19 22 58 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
60 59 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
61 60 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
62 13 ffnd ⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) Fn 𝐴 )
63 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) Fn 𝐴 )
64 elpreima ⊢ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) Fn 𝐴 → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
65 63 64 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
66 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → 𝐹 Fn 𝐴 )
68 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
69 67 68 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
70 61 65 69 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
71 70 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) = ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
72 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ∈ dom vol )
73 1 3 72 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ∈ dom vol )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ∈ dom vol )
75 71 74 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
76 elioomnf ⊢ ( 𝑦 ∈ ℝ* → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ) ) )
77 17 76 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ) ) )
78 21 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ) ) )
79 24 biantrurd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
80 33 breq1d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ) )
81 39 breq2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( - 𝑦 < ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ↔ - 𝑦 < - ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
82 51 breq1d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( - 𝑦 / - 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) )
83 ltdivmul ⊢ ( ( - 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( - 𝐵 ∈ ℝ ∧ 0 < - 𝐵 ) ) → ( ( - 𝑦 / - 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ - 𝑦 < ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
84 41 24 42 45 83 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( - 𝑦 / - 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ - 𝑦 < ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
85 82 84 bitr3d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ - 𝑦 < ( - 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
86 35 16 ltnegd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ↔ - 𝑦 < - ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
87 81 85 86 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ) )
88 80 87 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) )
89 elioopnf ⊢ ( ( 𝑦 / 𝐵 ) ∈ ℝ* → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
90 55 89 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
91 79 88 90 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
92 77 78 91 3bitr2d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
93 92 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
94 93 pm5.32da ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
95 elpreima ⊢ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) Fn 𝐴 → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
96 63 95 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
97 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑧 ∈ ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
98 67 97 syl ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
99 94 96 98 3bitr4d ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
100 99 eqrdv ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) = ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
101 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : 𝐴 ⟶ ℝ ) → ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ∈ dom vol )
102 1 3 101 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ∈ dom vol )
103 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ∈ dom vol )
104 100 103 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐵 < 0 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
105 14 15 75 104 ismbf2d ⊢ ( ( 𝜑 ∧ 𝐵 < 0 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )
106 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → 𝐴 ∈ dom vol )
107 3 adantr ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → 𝐹 : 𝐴 ⟶ ℝ )
108 simpr ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → 𝐵 = 0 )
109 0cn ⊢ 0 ∈ ℂ
110 108 109 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → 𝐵 ∈ ℂ )
111 0cnd ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → 0 ∈ ℂ )
112 simplr ⊢ ( ( ( 𝜑 ∧ 𝐵 = 0 ) ∧ 𝑥 ∈ ℝ ) → 𝐵 = 0 )
113 112 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝐵 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 · 𝑥 ) = ( 0 · 𝑥 ) )
114 mul02lem2 ⊢ ( 𝑥 ∈ ℝ → ( 0 · 𝑥 ) = 0 )
115 114 adantl ⊢ ( ( ( 𝜑 ∧ 𝐵 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 0 · 𝑥 ) = 0 )
116 113 115 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐵 = 0 ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 · 𝑥 ) = 0 )
117 106 107 110 111 116 caofid2 ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) = ( 𝐴 × { 0 } ) )
118 mbfconst ⊢ ( ( 𝐴 ∈ dom vol ∧ 0 ∈ ℂ ) → ( 𝐴 × { 0 } ) ∈ MblFn )
119 106 109 118 sylancl ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( 𝐴 × { 0 } ) ∈ MblFn )
120 117 119 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐵 = 0 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )
121 13 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) : 𝐴 ⟶ ℝ )
122 11 adantr ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → 𝐴 ∈ dom vol )
123 simprl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
124 123 rexrd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ* )
125 124 18 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ) ) )
126 20 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ )
127 126 biantrurd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ) ) )
128 23 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
129 128 biantrurd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
130 eqidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
131 11 2 66 130 ofc1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) )
132 131 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) = ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) )
133 132 breq2d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
134 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ )
135 simplr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 0 < 𝐵 )
136 ltdivmul ⊢ ( ( 𝑦 ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
137 123 128 134 135 136 syl112anc ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ↔ 𝑦 < ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) ) )
138 133 137 bitr4d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) )
139 134 135 elrpd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → 𝐵 ∈ ℝ+ )
140 123 139 rerpdivcld ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 / 𝐵 ) ∈ ℝ )
141 140 rexrd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 / 𝐵 ) ∈ ℝ* )
142 141 89 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝑦 / 𝐵 ) < ( 𝐹 ‘ 𝑧 ) ) ) )
143 129 138 142 3bitr4d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 < ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
144 125 127 143 3bitr2d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
145 144 anassrs ⊢ ( ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
146 145 pm5.32da ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
147 62 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) Fn 𝐴 )
148 147 64 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( 𝑦 (,) +∞ ) ) ) )
149 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → 𝐹 Fn 𝐴 )
150 149 97 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
151 146 148 150 3bitr4d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ) )
152 151 eqrdv ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) = ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) )
153 102 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( ( 𝑦 / 𝐵 ) (,) +∞ ) ) ∈ dom vol )
154 152 153 eqeltrd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( 𝑦 (,) +∞ ) ) ∈ dom vol )
155 124 76 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ) ) )
156 126 biantrurd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ℝ ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ) ) )
157 ltmuldiv2 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → ( ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) )
158 128 123 134 135 157 syl112anc ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) )
159 132 breq1d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( 𝐵 · ( 𝐹 ‘ 𝑧 ) ) < 𝑦 ) )
160 141 56 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) ) )
161 128 160 mpbirand ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ↔ ( 𝐹 ‘ 𝑧 ) < ( 𝑦 / 𝐵 ) ) )
162 158 159 161 3bitr4d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) < 𝑦 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
163 155 156 162 3bitr2d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ 𝐴 ) ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
164 163 anassrs ⊢ ( ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
165 164 pm5.32da ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
166 147 95 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ‘ 𝑧 ) ∈ ( -∞ (,) 𝑦 ) ) ) )
167 149 68 syl ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ↔ ( 𝑧 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
168 165 166 167 3bitr4d ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( 𝑧 ∈ ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ↔ 𝑧 ∈ ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ) )
169 168 eqrdv ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) = ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) )
170 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ 𝐹 “ ( -∞ (,) ( 𝑦 / 𝐵 ) ) ) ∈ dom vol )
171 169 170 eqeltrd ⊢ ( ( ( 𝜑 ∧ 0 < 𝐵 ) ∧ 𝑦 ∈ ℝ ) → ( ◡ ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) “ ( -∞ (,) 𝑦 ) ) ∈ dom vol )
172 121 122 154 171 ismbf2d ⊢ ( ( 𝜑 ∧ 0 < 𝐵 ) → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )
173 0re ⊢ 0 ∈ ℝ
174 lttri4 ⊢ ( ( 𝐵 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵 ) )
175 2 173 174 sylancl ⊢ ( 𝜑 → ( 𝐵 < 0 ∨ 𝐵 = 0 ∨ 0 < 𝐵 ) )
176 105 120 172 175 mpjao3dan ⊢ ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )