Theorem smfneg

Description: The negative of a sigma-measurable function is measurable. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	smfneg.x	$$⊢Ⅎx\phi$$
	smfneg.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
	smfneg.a	$$⊢\phi \to A\in V$$
	smfneg.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	smfneg.m	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
Assertion	smfneg	$$⊢\phi \to \left(x\in A⟼-B\right)\in \mathrm{SMblFn}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		smfneg.x	$$⊢Ⅎx\phi$$
2		smfneg.s	$$⊢\phi \to S\in \mathrm{SAlg}$$
3		smfneg.a	$$⊢\phi \to A\in V$$
4		smfneg.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
5		smfneg.m	$$⊢\phi \to \left(x\in A⟼B\right)\in \mathrm{SMblFn}\left(S\right)$$
6	4	recnd	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
7	6	mulm1d	$$⊢\left(\phi \wedge x\in A\right)\to -1B=-B$$
8	7	eqcomd	$$⊢\left(\phi \wedge x\in A\right)\to -B=-1B$$
9	1 8	mpteq2da	$$⊢\phi \to \left(x\in A⟼-B\right)=\left(x\in A⟼-1B\right)$$
10		neg1rr	$$⊢-1\in ℝ$$
11	10	a1i	$$⊢\phi \to -1\in ℝ$$
12	1 2 3 4 11 5	smfmulc1	$$⊢\phi \to \left(x\in A⟼-1B\right)\in \mathrm{SMblFn}\left(S\right)$$
13	9 12	eqeltrd	$$⊢\phi \to \left(x\in A⟼-B\right)\in \mathrm{SMblFn}\left(S\right)$$