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
|- ( ph -> A C_ RR )
mbfeqa.2
|- ( ph -> ( vol* ` A ) = 0 )
mbfeqa.3
|- ( ( ph /\ x e. ( B \ A ) ) -> C = D )
mbfeqa.4
|- ( ( ph /\ x e. B ) -> C e. CC )
mbfeqa.5
|- ( ( ph /\ x e. B ) -> D e. CC )
Assertion mbfeqa
|- ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )

Proof

Step Hyp Ref Expression
1 mbfeqa.1
 |-  ( ph -> A C_ RR )
2 mbfeqa.2
 |-  ( ph -> ( vol* ` A ) = 0 )
3 mbfeqa.3
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = D )
4 mbfeqa.4
 |-  ( ( ph /\ x e. B ) -> C e. CC )
5 mbfeqa.5
 |-  ( ( ph /\ x e. B ) -> D e. CC )
6 3 fveq2d
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Re ` C ) = ( Re ` D ) )
7 4 recld
 |-  ( ( ph /\ x e. B ) -> ( Re ` C ) e. RR )
8 5 recld
 |-  ( ( ph /\ x e. B ) -> ( Re ` D ) e. RR )
9 1 2 6 7 8 mbfeqalem2
 |-  ( ph -> ( ( x e. B |-> ( Re ` C ) ) e. MblFn <-> ( x e. B |-> ( Re ` D ) ) e. MblFn ) )
10 3 fveq2d
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Im ` C ) = ( Im ` D ) )
11 4 imcld
 |-  ( ( ph /\ x e. B ) -> ( Im ` C ) e. RR )
12 5 imcld
 |-  ( ( ph /\ x e. B ) -> ( Im ` D ) e. RR )
13 1 2 10 11 12 mbfeqalem2
 |-  ( ph -> ( ( x e. B |-> ( Im ` C ) ) e. MblFn <-> ( x e. B |-> ( Im ` D ) ) e. MblFn ) )
14 9 13 anbi12d
 |-  ( ph -> ( ( ( x e. B |-> ( Re ` C ) ) e. MblFn /\ ( x e. B |-> ( Im ` C ) ) e. MblFn ) <-> ( ( x e. B |-> ( Re ` D ) ) e. MblFn /\ ( x e. B |-> ( Im ` D ) ) e. MblFn ) ) )
15 4 ismbfcn2
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( ( x e. B |-> ( Re ` C ) ) e. MblFn /\ ( x e. B |-> ( Im ` C ) ) e. MblFn ) ) )
16 5 ismbfcn2
 |-  ( ph -> ( ( x e. B |-> D ) e. MblFn <-> ( ( x e. B |-> ( Re ` D ) ) e. MblFn /\ ( x e. B |-> ( Im ` D ) ) e. MblFn ) ) )
17 14 15 16 3bitr4d
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( x e. B |-> D ) e. MblFn ) )