Metamath Proof Explorer

Theorem mbfmulc2

Description: A complex constant times a measurable function is measurable. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses mbfmulc2.1 
|- ( ph -> C e. CC )
mbfmulc2.2 
|- ( ( ph /\ x e. A ) -> B e. V )
mbfmulc2.3 
|- ( ph -> ( x e. A |-> B ) e. MblFn )
Assertion mbfmulc2 
|- ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfmulc2.1 
 |-  ( ph -> C e. CC )
2 mbfmulc2.2 
 |-  ( ( ph /\ x e. A ) -> B e. V )
3 mbfmulc2.3 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
4 3 2 mbfdm2 
 |-  ( ph -> A e. dom vol )
5 1 recld 
 |-  ( ph -> ( Re ` C ) e. RR )
6 5 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR )
7 6 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC )
8 3 2 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
9 8 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
10 9 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
11 7 10 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Re ` B ) ) e. CC )
12 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) e. _V )
13 fconstmpt 
 |-  ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) )
14 13 a1i 
 |-  ( ph -> ( A X. { ( Re ` C ) } ) = ( x e. A |-> ( Re ` C ) ) )
15 eqidd 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) = ( x e. A |-> ( Re ` B ) ) )
16 4 6 9 14 15 offval2 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Re ` B ) ) ) )
17 1 imcld 
 |-  ( ph -> ( Im ` C ) e. RR )
18 17 renegcld 
 |-  ( ph -> -u ( Im ` C ) e. RR )
19 18 adantr 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. RR )
20 8 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
21 fconstmpt 
 |-  ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) )
22 21 a1i 
 |-  ( ph -> ( A X. { -u ( Im ` C ) } ) = ( x e. A |-> -u ( Im ` C ) ) )
23 eqidd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) = ( x e. A |-> ( Im ` B ) ) )
24 4 19 20 22 23 offval2 
 |-  ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( -u ( Im ` C ) x. ( Im ` B ) ) ) )
25 4 11 12 16 24 offval2 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) ) )
26 17 adantr 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR )
27 26 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC )
28 20 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
29 27 28 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Im ` B ) ) e. CC )
30 11 29 negsubd 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + -u ( ( Im ` C ) x. ( Im ` B ) ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) )
31 27 28 mulneg1d 
 |-  ( ( ph /\ x e. A ) -> ( -u ( Im ` C ) x. ( Im ` B ) ) = -u ( ( Im ` C ) x. ( Im ` B ) ) )
32 31 oveq2d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) + -u ( ( Im ` C ) x. ( Im ` B ) ) ) )
33 1 adantr 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
34 33 8 remuld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Re ` B ) ) - ( ( Im ` C ) x. ( Im ` B ) ) ) )
35 30 32 34 3eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) = ( Re ` ( C x. B ) ) )
36 35 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( ( ( Re ` C ) x. ( Re ` B ) ) + ( -u ( Im ` C ) x. ( Im ` B ) ) ) ) = ( x e. A |-> ( Re ` ( C x. B ) ) ) )
37 25 36 eqtrd 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) = ( x e. A |-> ( Re ` ( C x. B ) ) ) )
38 8 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
39 3 38 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) )
40 39 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
41 10 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) : A --> CC )
42 40 5 41 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn )
43 39 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
44 28 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) : A --> CC )
45 43 18 44 mbfmulc2re 
 |-  ( ph -> ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn )
46 42 45 mbfadd 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) oF + ( ( A X. { -u ( Im ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) ) e. MblFn )
47 37 46 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( Re ` ( C x. B ) ) ) e. MblFn )
48 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( ( Re ` C ) x. ( Im ` B ) ) e. _V )
49 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( ( Im ` C ) x. ( Re ` B ) ) e. _V )
50 4 6 20 14 23 offval2 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) = ( x e. A |-> ( ( Re ` C ) x. ( Im ` B ) ) ) )
51 fconstmpt 
 |-  ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) )
52 51 a1i 
 |-  ( ph -> ( A X. { ( Im ` C ) } ) = ( x e. A |-> ( Im ` C ) ) )
53 4 26 9 52 15 offval2 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) = ( x e. A |-> ( ( Im ` C ) x. ( Re ` B ) ) ) )
54 4 48 49 50 53 offval2 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) )
55 33 8 immuld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( C x. B ) ) = ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) )
56 55 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Im ` ( C x. B ) ) ) = ( x e. A |-> ( ( ( Re ` C ) x. ( Im ` B ) ) + ( ( Im ` C ) x. ( Re ` B ) ) ) ) )
57 54 56 eqtr4d 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) = ( x e. A |-> ( Im ` ( C x. B ) ) ) )
58 43 5 44 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) e. MblFn )
59 40 17 41 mbfmulc2re 
 |-  ( ph -> ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) e. MblFn )
60 58 59 mbfadd 
 |-  ( ph -> ( ( ( A X. { ( Re ` C ) } ) oF x. ( x e. A |-> ( Im ` B ) ) ) oF + ( ( A X. { ( Im ` C ) } ) oF x. ( x e. A |-> ( Re ` B ) ) ) ) e. MblFn )
61 57 60 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( Im ` ( C x. B ) ) ) e. MblFn )
62 33 8 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( C x. B ) e. CC )
63 62 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> ( C x. B ) ) e. MblFn <-> ( ( x e. A |-> ( Re ` ( C x. B ) ) ) e. MblFn /\ ( x e. A |-> ( Im ` ( C x. B ) ) ) e. MblFn ) ) )
64 47 61 63 mpbir2and 
 |-  ( ph -> ( x e. A |-> ( C x. B ) ) e. MblFn )