This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )