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