Metamath Proof Explorer


Theorem mbfmulc2lem

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

Ref Expression
Hypotheses mbfmulc2re.1 φ F MblFn
mbfmulc2re.2 φ B
mbfmulc2lem.3 φ F : A
Assertion mbfmulc2lem φ A × B × f F MblFn

Proof

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