Theorem mbfneg

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

	Ref	Expression
Hypotheses	mbfneg.1	|- ( ( ph /\ x e. A ) -> B e. V )
	mbfneg.2	|- ( ph -> ( x e. A |-> B ) e. MblFn )
Assertion	mbfneg	|- ( ph -> ( x e. A |-> -u B ) e. MblFn )

Proof

Step	Hyp	Ref	Expression
1		mbfneg.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		mbfneg.2	|- ( ph -> ( x e. A |-> B ) e. MblFn )
3		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
4	3 1	dmmptd	|- ( ph -> dom ( x e. A |-> B ) = A )
5	2	dmexd	|- ( ph -> dom ( x e. A |-> B ) e. _V )
6	4 5	eqeltrrd	|- ( ph -> A e. _V )
7		neg1rr	|- -u 1 e. RR
8	7	a1i	|- ( ( ph /\ x e. A ) -> -u 1 e. RR )
9		fconstmpt	|- ( A X. { -u 1 } ) = ( x e. A |-> -u 1 )
10	9	a1i	|- ( ph -> ( A X. { -u 1 } ) = ( x e. A |-> -u 1 ) )
11		eqidd	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> B ) )
12	6 8 1 10 11	offval2	|- ( ph -> ( ( A X. { -u 1 } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> ( -u 1 x. B ) ) )
13	2 1	mbfmptcl	|- ( ( ph /\ x e. A ) -> B e. CC )
14	13	mulm1d	|- ( ( ph /\ x e. A ) -> ( -u 1 x. B ) = -u B )
15	14	mpteq2dva	|- ( ph -> ( x e. A |-> ( -u 1 x. B ) ) = ( x e. A |-> -u B ) )
16	12 15	eqtrd	|- ( ph -> ( ( A X. { -u 1 } ) oF x. ( x e. A |-> B ) ) = ( x e. A |-> -u B ) )
17	7	a1i	|- ( ph -> -u 1 e. RR )
18	13	fmpttd	|- ( ph -> ( x e. A |-> B ) : A --> CC )
19	2 17 18	mbfmulc2re	|- ( ph -> ( ( A X. { -u 1 } ) oF x. ( x e. A |-> B ) ) e. MblFn )
20	16 19	eqeltrrd	|- ( ph -> ( x e. A |-> -u B ) e. MblFn )