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 ) )