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