Metamath Proof Explorer

Theorem mbfmul

Description: The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

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

Proof

Step Hyp Ref Expression
1 mbfmul.1 
 |-  ( ph -> F e. MblFn )
2 mbfmul.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 x. G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) 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 remuld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( ( F ` x ) x. ( G ` x ) ) ) = ( ( ( Re ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) - ( ( Im ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) ) )
24 23 mpteq2dva 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) x. ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( ( Re ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) - ( ( Im ` ( F ` x ) ) x. ( Im ` ( 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 ovexd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( Re ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) e. _V )
28 ovexd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( Im ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) e. _V )
29 19 recld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( F ` x ) ) e. RR )
30 22 recld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Re ` ( G ` x ) ) e. RR )
31 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) )
32 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) )
33 26 29 30 31 32 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Re ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) ) )
34 19 imcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( F ` x ) ) e. RR )
35 22 imcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( G ` x ) ) e. RR )
36 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) )
37 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) )
38 26 34 35 36 37 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Im ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) ) )
39 26 27 28 33 38 offval2 
 |-  ( ph -> ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) oF - ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( ( Re ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) - ( ( Im ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) ) ) )
40 24 39 eqtr4d 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) x. ( G ` x ) ) ) ) = ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) oF - ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) ) )
41 inss1 
 |-  ( dom F i^i dom G ) C_ dom F
42 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 ) ) )
43 41 42 ax-mp 
 |-  ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) )
44 4 feqmptd 
 |-  ( ph -> F = ( x e. dom F |-> ( F ` x ) ) )
45 44 1 eqeltrrd 
 |-  ( ph -> ( x e. dom F |-> ( F ` x ) ) e. MblFn )
46 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 )
47 45 26 46 syl2anc 
 |-  ( ph -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
48 43 47 eqeltrrid 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) e. MblFn )
49 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 ) ) )
50 48 49 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 ) )
51 50 simpld 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) e. MblFn )
52 inss2 
 |-  ( dom F i^i dom G ) C_ dom G
53 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 ) ) )
54 52 53 ax-mp 
 |-  ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( G ` x ) )
55 7 feqmptd 
 |-  ( ph -> G = ( x e. dom G |-> ( G ` x ) ) )
56 55 2 eqeltrrd 
 |-  ( ph -> ( x e. dom G |-> ( G ` x ) ) e. MblFn )
57 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 )
58 56 26 57 syl2anc 
 |-  ( ph -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
59 54 58 eqeltrrid 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) e. MblFn )
60 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 ) ) )
61 59 60 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 ) )
62 61 simpld 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) e. MblFn )
63 29 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) : ( dom F i^i dom G ) --> RR )
64 30 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) : ( dom F i^i dom G ) --> RR )
65 51 62 63 64 mbfmullem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) e. MblFn )
66 50 simprd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) e. MblFn )
67 61 simprd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) e. MblFn )
68 34 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) : ( dom F i^i dom G ) --> RR )
69 35 fmpttd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) : ( dom F i^i dom G ) --> RR )
70 66 67 68 69 mbfmullem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) e. MblFn )
71 65 70 mbfsub 
 |-  ( ph -> ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) oF - ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) ) e. MblFn )
72 40 71 eqeltrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) x. ( G ` x ) ) ) ) e. MblFn )
73 19 22 immuld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( Im ` ( ( F ` x ) x. ( G ` x ) ) ) = ( ( ( Re ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) + ( ( Im ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) ) )
74 73 mpteq2dva 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) x. ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( ( Re ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) + ( ( Im ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) ) ) )
75 ovexd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( Re ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) e. _V )
76 ovexd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( Im ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) e. _V )
77 26 29 35 31 37 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Re ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) ) )
78 26 34 30 36 32 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( Im ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) ) )
79 26 75 76 77 78 offval2 
 |-  ( ph -> ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) oF + ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( ( Re ` ( F ` x ) ) x. ( Im ` ( G ` x ) ) ) + ( ( Im ` ( F ` x ) ) x. ( Re ` ( G ` x ) ) ) ) ) )
80 74 79 eqtr4d 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) x. ( G ` x ) ) ) ) = ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) oF + ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) ) )
81 51 67 63 69 mbfmullem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) e. MblFn )
82 66 62 68 64 mbfmullem 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) e. MblFn )
83 81 82 mbfadd 
 |-  ( ph -> ( ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Im ` ( G ` x ) ) ) ) oF + ( ( x e. ( dom F i^i dom G ) |-> ( Im ` ( F ` x ) ) ) oF x. ( x e. ( dom F i^i dom G ) |-> ( Re ` ( G ` x ) ) ) ) ) e. MblFn )
84 80 83 eqeltrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) x. ( G ` x ) ) ) ) e. MblFn )
85 19 22 mulcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( F ` x ) x. ( G ` x ) ) e. CC )
86 85 ismbfcn2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) ) e. MblFn <-> ( ( x e. ( dom F i^i dom G ) |-> ( Re ` ( ( F ` x ) x. ( G ` x ) ) ) ) e. MblFn /\ ( x e. ( dom F i^i dom G ) |-> ( Im ` ( ( F ` x ) x. ( G ` x ) ) ) ) e. MblFn ) ) )
87 72 84 86 mpbir2and 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) x. ( G ` x ) ) ) e. MblFn )
88 16 87 eqeltrd 
 |-  ( ph -> ( F oF x. G ) e. MblFn )