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\times \left\{-1\right\}=\left(x\in A⟼-1\right)$$
10	9	a1i	$$⊢\phi \to A\times \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\times \left\{-1\right\}\right){\times }_f\left(x\in A⟼B\right)=\left(x\in A⟼-1B\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 -1B=-B$$
15	14	mpteq2dva	$$⊢\phi \to \left(x\in A⟼-1B\right)=\left(x\in A⟼-B\right)$$
16	12 15	eqtrd	$$⊢\phi \to \left(A\times \left\{-1\right\}\right){\times }_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\times \left\{-1\right\}\right){\times }_f\left(x\in A⟼B\right)\in MblFn$$
20	16 19	eqeltrrd	$$⊢\phi \to \left(x\in A⟼-B\right)\in MblFn$$