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 )`
` |-  ( ( 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 )`
` |-  ( ( ph /\ B < 0 ) -> ( ( A X. { B } ) oF x. F ) : A --> RR )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ B < 0 ) /\ ( y e. RR /\ z e. A ) ) -> A e. dom vol )`
` |-  ( ( ( ph /\ B < 0 ) /\ ( y e. RR /\ z e. A ) ) -> B e. RR )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ph /\ B = 0 ) -> A e. dom vol )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ph /\ 0 < B ) -> ( ( A X. { B } ) oF x. F ) : A --> RR )`
` |-  ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( 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 ) ) )`
` |-  ( ( ( 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 ) ) ) )`
` |-  ( ( ( ph /\ 0 < B ) /\ y e. RR ) -> ( `' F " ( -oo (,) ( y / B ) ) ) e. dom vol )`
` |-  ( ( ( ph /\ 0 < B ) /\ y e. RR ) -> ( `' ( ( A X. { B } ) oF x. F ) " ( -oo (,) y ) ) e. dom vol )`
` |-  ( ( ph /\ 0 < B ) -> ( ( A X. { B } ) oF x. F ) e. MblFn )`
` |-  0 e. RR`
` |-  ( ( B e. RR /\ 0 e. RR ) -> ( B < 0 \/ B = 0 \/ 0 < B ) )`
` |-  ( ph -> ( B < 0 \/ B = 0 \/ 0 < B ) )`
` |-  ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )`