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

Metamath Proof Explorer

Theorem mbfeqa

Description: If two functions are equal almost everywhere, then one is measurable iff the other is. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses mbfeqa.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
mbfeqa.2 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
mbfeqa.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
mbfeqa.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
mbfeqa.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
Assertion mbfeqa ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ) )

Proof

Step Hyp Ref Expression
1 mbfeqa.1 ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2 mbfeqa.2 ⊢ ( 𝜑 → ( vol* ‘ 𝐴 ) = 0 )
3 mbfeqa.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 𝐷 )
4 mbfeqa.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
5 mbfeqa.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐷 ∈ ℂ )
6 3 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℜ ‘ 𝐶 ) = ( ℜ ‘ 𝐷 ) )
7 4 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
8 5 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ 𝐷 ) ∈ ℝ )
9 1 2 6 7 8 mbfeqalem2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐷 ) ) ∈ MblFn ) )
10 3 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → ( ℑ ‘ 𝐶 ) = ( ℑ ‘ 𝐷 ) )
11 4 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
12 5 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℑ ‘ 𝐷 ) ∈ ℝ )
13 1 2 10 11 12 mbfeqalem2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐷 ) ) ∈ MblFn ) )
14 9 13 anbi12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐷 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐷 ) ) ∈ MblFn ) ) )
15 4 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ) )
16 5 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐵 ↦ ( ℜ ‘ 𝐷 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐵 ↦ ( ℑ ‘ 𝐷 ) ) ∈ MblFn ) ) )
17 14 15 16 3bitr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ↔ ( 𝑥 ∈ 𝐵 ↦ 𝐷 ) ∈ MblFn ) )