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 )