Theorem mbfneg

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

	Ref	Expression
Hypotheses	mbfneg.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	mbfneg.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
Assertion	mbfneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ MblFn )

Proof

Step	Hyp	Ref	Expression
1		mbfneg.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		mbfneg.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
3		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	3 1	dmmptd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
5	2	dmexd	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
6	4 5	eqeltrrd	⊢ ( 𝜑 → 𝐴 ∈ V )
7		neg1rr	⊢ - 1 ∈ ℝ
8	7	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 1 ∈ ℝ )
9		fconstmpt	⊢ ( 𝐴 × { - 1 } ) = ( 𝑥 ∈ 𝐴 ↦ - 1 )
10	9	a1i	⊢ ( 𝜑 → ( 𝐴 × { - 1 } ) = ( 𝑥 ∈ 𝐴 ↦ - 1 ) )
11		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
12	6 8 1 10 11	offval2	⊢ ( 𝜑 → ( ( 𝐴 × { - 1 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝐵 ) ) )
13	2 1	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
14	13	mulm1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · 𝐵 ) = - 𝐵 )
15	14	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
16	12 15	eqtrd	⊢ ( 𝜑 → ( ( 𝐴 × { - 1 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) )
17	7	a1i	⊢ ( 𝜑 → - 1 ∈ ℝ )
18	13	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
19	2 17 18	mbfmulc2re	⊢ ( 𝜑 → ( ( 𝐴 × { - 1 } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) ∈ MblFn )
20	16 19	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ MblFn )