Metamath Proof Explorer

Theorem mbfadd

Description: The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfadd.1 
|- ( ph -> F e. MblFn )
mbfadd.2 
|- ( ph -> G e. MblFn )
Assertion mbfadd 
|- ( ph -> ( F oF + G ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfadd.1 
 |-  ( ph -> F e. MblFn )
2 mbfadd.2 
 |-  ( ph -> G e. MblFn )
3 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
4 1 3 syl 
 |-  ( ph -> F : dom F --> CC )
5 4 ffnd 
 |-  ( ph -> F Fn dom F )
6 mbff 
 |-  ( G e. MblFn -> G : dom G --> CC )
7 2 6 syl 
 |-  ( ph -> G : dom G --> CC )
8 7 ffnd 
 |-  ( ph -> G Fn dom G )
9 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
10 1 9 syl 
 |-  ( ph -> dom F e. dom vol )
11 mbfdm 
 |-  ( G e. MblFn -> dom G e. dom vol )
12 2 11 syl 
 |-  ( ph -> dom G e. dom vol )
13 eqid 
 |-  ( dom F i^i dom G ) = ( dom F i^i dom G )
14 eqidd 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` x ) = ( F ` x ) )
15 eqidd 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) = ( G ` x ) )
16 5 8 10 12 13 14 15 offval 
 |-  ( ph -> ( F oF + G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + ( G ` x ) ) ) )
17 elinel1 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom F )
18 ffvelrn 
 |-  ( ( F : dom F --> CC /\ x e. dom F ) -> ( F ` x ) e. CC )
19 4 17 18 syl2an 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( F ` x ) e. CC )
20 elinel2 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom G )
21 ffvelrn 
 |-  ( ( G : dom G --> CC /\ x e. dom G ) -> ( G ` x ) e. CC )
22 7 20 21 syl2an 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( G ` x ) e. CC )
23 19 22 readdd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( ( F ` x ) + ( G ` x ) ) ) = ( ( Re ` ( F ` x ) ) + ( Re ` ( G ` x ) ) ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) + ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Re ` ( F ` x ) ) + ( Re ` ( G ` x ) ) ) ) )
25 inmbl 
 |-  ( ( dom F e. dom vol /\ dom G e. dom vol ) -> ( dom F i^i dom G ) e. dom vol )
26 10 12 25 syl2anc 
 |-  ( ph -> ( dom F i^i dom G ) e. dom vol )
27 19 recld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( F ` x ) ) e. RR )
28 22 recld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( G ` x ) ) e. RR )
29 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) )
30 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) )
31 26 27 28 29 30 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Re ` ( F ` x ) ) + ( Re ` ( G ` x ) ) ) ) )
32 24 31 eqtr4d 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) + ( G ` x ) ) ) ) = ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) )
33 inss1 
 |-  ( dom F i^i dom G ) C_ dom F
34 resmpt 
 |-  ( ( dom F i^i dom G ) C_ dom F -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) )
35 33 34 ax-mp 
 |-  ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) )
36 4 feqmptd 
 |-  ( ph -> F = ( x e. dom F |-> ( F ` x ) ) )
37 36 1 eqeltrrd 
 |-  ( ph -> ( x e. dom F |-> ( F ` x ) ) e. MblFn )
38 mbfres 
 |-  ( ( ( x e. dom F |-> ( F ` x ) ) e. MblFn /\ ( dom F i^i dom G ) e. dom vol ) -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
39 37 26 38 syl2anc 
 |-  ( ph -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
40 35 39 eqeltrrid 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) e. MblFn )
41 19 ismbfcn2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) e. MblFn <-> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) e. MblFn ) ) )
42 40 41 mpbid 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) e. MblFn ) )
43 42 simpld 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) e. MblFn )
44 inss2 
 |-  ( dom F i^i dom G ) C_ dom G
45 resmpt 
 |-  ( ( dom F i^i dom G ) C_ dom G -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) )
46 44 45 ax-mp 
 |-  ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( G ` x ) )
47 7 feqmptd 
 |-  ( ph -> G = ( x e. dom G |-> ( G ` x ) ) )
48 47 2 eqeltrrd 
 |-  ( ph -> ( x e. dom G |-> ( G ` x ) ) e. MblFn )
49 mbfres 
 |-  ( ( ( x e. dom G |-> ( G ` x ) ) e. MblFn /\ ( dom F i^i dom G ) e. dom vol ) -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
50 48 26 49 syl2anc 
 |-  ( ph -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
51 46 50 eqeltrrid 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) e. MblFn )
52 22 ismbfcn2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) e. MblFn <-> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) e. MblFn ) ) )
53 51 52 mpbid 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) e. MblFn ) )
54 53 simpld 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) e. MblFn )
55 27 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) : ( dom F i^i dom G ) --> RR )
56 28 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) : ( dom F i^i dom G ) --> RR )
57 43 54 55 56 mbfaddlem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) e. MblFn )
58 32 57 eqeltrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) + ( G ` x ) ) ) ) e. MblFn )
59 19 22 imaddd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( ( F ` x ) + ( G ` x ) ) ) = ( ( Im ` ( F ` x ) ) + ( Im ` ( G ` x ) ) ) )
60 59 mpteq2dva 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) + ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Im ` ( F ` x ) ) + ( Im ` ( G ` x ) ) ) ) )
61 19 imcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( F ` x ) ) e. RR )
62 22 imcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( G ` x ) ) e. RR )
63 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) )
64 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) )
65 26 61 62 63 64 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Im ` ( F ` x ) ) + ( Im ` ( G ` x ) ) ) ) )
66 60 65 eqtr4d 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) + ( G ` x ) ) ) ) = ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) )
67 42 simprd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) e. MblFn )
68 53 simprd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) e. MblFn )
69 61 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) : ( dom F i^i dom G ) --> RR )
70 62 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) : ( dom F i^i dom G ) --> RR )
71 67 68 69 70 mbfaddlem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF + ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) e. MblFn )
72 66 71 eqeltrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) + ( G ` x ) ) ) ) e. MblFn )
73 19 22 addcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( F ` x ) + ( G ` x ) ) e. CC )
74 73 ismbfcn2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + ( G ` x ) ) ) e. MblFn <-> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) + ( G ` x ) ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) + ( G ` x ) ) ) ) e. MblFn ) ) )
75 58 72 74 mpbir2and 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + ( G ` x ) ) ) e. MblFn )
76 16 75 eqeltrd 
 |-  ( ph -> ( F oF + G ) e. MblFn )