# Metamath Proof Explorer

## Theorem mbfmulc2lem

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

Ref Expression
Hypotheses mbfmulc2re.1 ${⊢}{\phi }\to {F}\in MblFn$
mbfmulc2re.2 ${⊢}{\phi }\to {B}\in ℝ$
mbfmulc2lem.3 ${⊢}{\phi }\to {F}:{A}⟶ℝ$
Assertion mbfmulc2lem ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}{F}\in MblFn$

### Proof

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