Theorem smfneg

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

	Ref	Expression
Hypotheses	smfneg.x	⊢ Ⅎ 𝑥 𝜑
	smfneg.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	smfneg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	smfneg.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	smfneg.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
Assertion	smfneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		smfneg.x	⊢ Ⅎ 𝑥 𝜑
2		smfneg.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
3		smfneg.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		smfneg.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		smfneg.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )
6	4	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
7	6	mulm1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - 1 · 𝐵 ) = - 𝐵 )
8	7	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐵 = ( - 1 · 𝐵 ) )
9	1 8	mpteq2da	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝐵 ) ) )
10		neg1rr	⊢ - 1 ∈ ℝ
11	10	a1i	⊢ ( 𝜑 → - 1 ∈ ℝ )
12	1 2 3 4 11 5	smfmulc1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( - 1 · 𝐵 ) ) ∈ ( SMblFn ‘ 𝑆 ) )
13	9 12	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐵 ) ∈ ( SMblFn ‘ 𝑆 ) )