Theorem smfneg

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

	Ref	Expression
Hypotheses	smfneg.x	|- F/ x ph
	smfneg.s	|- ( ph -> S e. SAlg )
	smfneg.a	|- ( ph -> A e. V )
	smfneg.b	|- ( ( ph /\ x e. A ) -> B e. RR )
	smfneg.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
Assertion	smfneg	|- ( ph -> ( x e. A |-> -u B ) e. ( SMblFn ` S ) )

Proof

Step	Hyp	Ref	Expression
1		smfneg.x	|- F/ x ph
2		smfneg.s	|- ( ph -> S e. SAlg )
3		smfneg.a	|- ( ph -> A e. V )
4		smfneg.b	|- ( ( ph /\ x e. A ) -> B e. RR )
5		smfneg.m	|- ( ph -> ( x e. A |-> B ) e. ( SMblFn ` S ) )
6	4	recnd	|- ( ( ph /\ x e. A ) -> B e. CC )
7	6	mulm1d	|- ( ( ph /\ x e. A ) -> ( -u 1 x. B ) = -u B )
8	7	eqcomd	|- ( ( ph /\ x e. A ) -> -u B = ( -u 1 x. B ) )
9	1 8	mpteq2da	|- ( ph -> ( x e. A |-> -u B ) = ( x e. A |-> ( -u 1 x. B ) ) )
10		neg1rr	|- -u 1 e. RR
11	10	a1i	|- ( ph -> -u 1 e. RR )
12	1 2 3 4 11 5	smfmulc1	|- ( ph -> ( x e. A |-> ( -u 1 x. B ) ) e. ( SMblFn ` S ) )
13	9 12	eqeltrd	|- ( ph -> ( x e. A |-> -u B ) e. ( SMblFn ` S ) )