Metamath Proof Explorer

Theorem mbfres2cn

Description: Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A , then F is measurable on the whole domain. Similar to mbfres2 but here the theorem is extended to complex-valued functions. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses mbfres2cn.f 
|- ( ph -> F : A --> CC )
mbfres2cn.b 
|- ( ph -> ( F |` B ) e. MblFn )
mbfres2cn.c 
|- ( ph -> ( F |` C ) e. MblFn )
mbfres2cn.a 
|- ( ph -> ( B u. C ) = A )
Assertion mbfres2cn 
|- ( ph -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfres2cn.f 
 |-  ( ph -> F : A --> CC )
2 mbfres2cn.b 
 |-  ( ph -> ( F |` B ) e. MblFn )
3 mbfres2cn.c 
 |-  ( ph -> ( F |` C ) e. MblFn )
4 mbfres2cn.a 
 |-  ( ph -> ( B u. C ) = A )
5 ref 
 |-  Re : CC --> RR
6 fco 
 |-  ( ( Re : CC --> RR /\ F : A --> CC ) -> ( Re o. F ) : A --> RR )
7 5 1 6 sylancr 
 |-  ( ph -> ( Re o. F ) : A --> RR )
8 resco 
 |-  ( ( Re o. F ) |` B ) = ( Re o. ( F |` B ) )
9 fresin 
 |-  ( F : A --> CC -> ( F |` B ) : ( A i^i B ) --> CC )
10 ismbfcn 
 |-  ( ( F |` B ) : ( A i^i B ) --> CC -> ( ( F |` B ) e. MblFn <-> ( ( Re o. ( F |` B ) ) e. MblFn /\ ( Im o. ( F |` B ) ) e. MblFn ) ) )
11 1 9 10 3syl 
 |-  ( ph -> ( ( F |` B ) e. MblFn <-> ( ( Re o. ( F |` B ) ) e. MblFn /\ ( Im o. ( F |` B ) ) e. MblFn ) ) )
12 2 11 mpbid 
 |-  ( ph -> ( ( Re o. ( F |` B ) ) e. MblFn /\ ( Im o. ( F |` B ) ) e. MblFn ) )
13 12 simpld 
 |-  ( ph -> ( Re o. ( F |` B ) ) e. MblFn )
14 8 13 eqeltrid 
 |-  ( ph -> ( ( Re o. F ) |` B ) e. MblFn )
15 resco 
 |-  ( ( Re o. F ) |` C ) = ( Re o. ( F |` C ) )
16 fresin 
 |-  ( F : A --> CC -> ( F |` C ) : ( A i^i C ) --> CC )
17 ismbfcn 
 |-  ( ( F |` C ) : ( A i^i C ) --> CC -> ( ( F |` C ) e. MblFn <-> ( ( Re o. ( F |` C ) ) e. MblFn /\ ( Im o. ( F |` C ) ) e. MblFn ) ) )
18 1 16 17 3syl 
 |-  ( ph -> ( ( F |` C ) e. MblFn <-> ( ( Re o. ( F |` C ) ) e. MblFn /\ ( Im o. ( F |` C ) ) e. MblFn ) ) )
19 3 18 mpbid 
 |-  ( ph -> ( ( Re o. ( F |` C ) ) e. MblFn /\ ( Im o. ( F |` C ) ) e. MblFn ) )
20 19 simpld 
 |-  ( ph -> ( Re o. ( F |` C ) ) e. MblFn )
21 15 20 eqeltrid 
 |-  ( ph -> ( ( Re o. F ) |` C ) e. MblFn )
22 7 14 21 4 mbfres2 
 |-  ( ph -> ( Re o. F ) e. MblFn )
23 imf 
 |-  Im : CC --> RR
24 fco 
 |-  ( ( Im : CC --> RR /\ F : A --> CC ) -> ( Im o. F ) : A --> RR )
25 23 1 24 sylancr 
 |-  ( ph -> ( Im o. F ) : A --> RR )
26 resco 
 |-  ( ( Im o. F ) |` B ) = ( Im o. ( F |` B ) )
27 12 simprd 
 |-  ( ph -> ( Im o. ( F |` B ) ) e. MblFn )
28 26 27 eqeltrid 
 |-  ( ph -> ( ( Im o. F ) |` B ) e. MblFn )
29 resco 
 |-  ( ( Im o. F ) |` C ) = ( Im o. ( F |` C ) )
30 19 simprd 
 |-  ( ph -> ( Im o. ( F |` C ) ) e. MblFn )
31 29 30 eqeltrid 
 |-  ( ph -> ( ( Im o. F ) |` C ) e. MblFn )
32 25 28 31 4 mbfres2 
 |-  ( ph -> ( Im o. F ) e. MblFn )
33 ismbfcn 
 |-  ( F : A --> CC -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
34 1 33 syl 
 |-  ( ph -> ( F e. MblFn <-> ( ( Re o. F ) e. MblFn /\ ( Im o. F ) e. MblFn ) ) )
35 22 32 34 mpbir2and 
 |-  ( ph -> F e. MblFn )