# Metamath Proof Explorer

## Theorem mbfneg

Description: The negative of a measurable function is measurable. (Contributed by Mario Carneiro, 31-Jul-2014)

Ref Expression
Hypotheses mbfneg.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
mbfneg.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in MblFn$
Assertion mbfneg ${⊢}{\phi }\to \left({x}\in {A}⟼-{B}\right)\in MblFn$

### Proof

Step Hyp Ref Expression
1 mbfneg.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
2 mbfneg.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in MblFn$
3 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
4 3 1 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
5 2 dmexd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)\in \mathrm{V}$
6 4 5 eqeltrrd ${⊢}{\phi }\to {A}\in \mathrm{V}$
7 neg1rr ${⊢}-1\in ℝ$
8 7 a1i ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -1\in ℝ$
9 fconstmpt ${⊢}{A}×\left\{-1\right\}=\left({x}\in {A}⟼-1\right)$
10 9 a1i ${⊢}{\phi }\to {A}×\left\{-1\right\}=\left({x}\in {A}⟼-1\right)$
11 eqidd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
12 6 8 1 10 11 offval2 ${⊢}{\phi }\to \left({A}×\left\{-1\right\}\right){×}_{f}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼-1{B}\right)$
13 2 1 mbfmptcl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
14 13 mulm1d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to -1{B}=-{B}$
15 14 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼-1{B}\right)=\left({x}\in {A}⟼-{B}\right)$
16 12 15 eqtrd ${⊢}{\phi }\to \left({A}×\left\{-1\right\}\right){×}_{f}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼-{B}\right)$
17 7 a1i ${⊢}{\phi }\to -1\in ℝ$
18 13 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right):{A}⟶ℂ$
19 2 17 18 mbfmulc2re ${⊢}{\phi }\to \left({A}×\left\{-1\right\}\right){×}_{f}\left({x}\in {A}⟼{B}\right)\in MblFn$
20 16 19 eqeltrrd ${⊢}{\phi }\to \left({x}\in {A}⟼-{B}\right)\in MblFn$