Metamath Proof Explorer

Theorem mbfmulc2lem

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

Ref Expression
Hypotheses mbfmulc2re.1 
|- ( ph -> F e. MblFn )
mbfmulc2re.2 
|- ( ph -> B e. RR )
mbfmulc2lem.3 
|- ( ph -> F : A --> RR )
Assertion mbfmulc2lem 
|- ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )

Proof

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