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 )