Metamath Proof Explorer

Theorem mbfmulc2re

Description: Multiplication by a constant preserves measurability. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfmulc2re.1 
|- ( ph -> F e. MblFn )
mbfmulc2re.2 
|- ( ph -> B e. RR )
mbfmulc2re.3 
|- ( ph -> F : A --> CC )
Assertion mbfmulc2re 
|- ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfmulc2re.1 
 |-  ( ph -> F e. MblFn )
2 mbfmulc2re.2 
 |-  ( ph -> B e. RR )
3 mbfmulc2re.3 
 |-  ( ph -> F : A --> CC )
4 3 fdmd 
 |-  ( ph -> dom F = A )
5 1 dmexd 
 |-  ( ph -> dom F e. _V )
6 4 5 eqeltrrd 
 |-  ( ph -> A e. _V )
7 2 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
8 3 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. CC )
9 fconstmpt 
 |-  ( A X. { B } ) = ( x e. A |-> B )
10 9 a1i 
 |-  ( ph -> ( A X. { B } ) = ( x e. A |-> B ) )
11 3 feqmptd 
 |-  ( ph -> F = ( x e. A |-> ( F ` x ) ) )
12 6 7 8 10 11 offval2 
 |-  ( ph -> ( ( A X. { B } ) oF x. F ) = ( x e. A |-> ( B x. ( F ` x ) ) ) )
13 7 8 remul2d 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B x. ( F ` x ) ) ) = ( B x. ( Re ` ( F ` x ) ) ) )
14 13 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Re ` ( B x. ( F ` x ) ) ) ) = ( x e. A |-> ( B x. ( Re ` ( F ` x ) ) ) ) )
15 8 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( F ` x ) ) e. RR )
16 eqidd 
 |-  ( ph -> ( x e. A |-> ( Re ` ( F ` x ) ) ) = ( x e. A |-> ( Re ` ( F ` x ) ) ) )
17 6 7 15 10 16 offval2 
 |-  ( ph -> ( ( A X. { B } ) oF x. ( x e. A |-> ( Re ` ( F ` x ) ) ) ) = ( x e. A |-> ( B x. ( Re ` ( F ` x ) ) ) ) )
18 14 17 eqtr4d 
 |-  ( ph -> ( x e. A |-> ( Re ` ( B x. ( F ` x ) ) ) ) = ( ( A X. { B } ) oF x. ( x e. A |-> ( Re ` ( F ` x ) ) ) ) )
19 11 1 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( F ` x ) ) e. MblFn )
20 8 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> ( F ` x ) ) e. MblFn <-> ( ( x e. A |-> ( Re ` ( F ` x ) ) ) e. MblFn /\ ( x e. A |-> ( Im ` ( F ` x ) ) ) e. MblFn ) ) )
21 19 20 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` ( F ` x ) ) ) e. MblFn /\ ( x e. A |-> ( Im ` ( F ` x ) ) ) e. MblFn ) )
22 21 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` ( F ` x ) ) ) e. MblFn )
23 15 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Re ` ( F ` x ) ) ) : A --> RR )
24 22 2 23 mbfmulc2lem 
 |-  ( ph -> ( ( A X. { B } ) oF x. ( x e. A |-> ( Re ` ( F ` x ) ) ) ) e. MblFn )
25 18 24 eqeltrd 
 |-  ( ph -> ( x e. A |-> ( Re ` ( B x. ( F ` x ) ) ) ) e. MblFn )
26 7 8 immul2d 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( B x. ( F ` x ) ) ) = ( B x. ( Im ` ( F ` x ) ) ) )
27 26 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Im ` ( B x. ( F ` x ) ) ) ) = ( x e. A |-> ( B x. ( Im ` ( F ` x ) ) ) ) )
28 8 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( F ` x ) ) e. RR )
29 eqidd 
 |-  ( ph -> ( x e. A |-> ( Im ` ( F ` x ) ) ) = ( x e. A |-> ( Im ` ( F ` x ) ) ) )
30 6 7 28 10 29 offval2 
 |-  ( ph -> ( ( A X. { B } ) oF x. ( x e. A |-> ( Im ` ( F ` x ) ) ) ) = ( x e. A |-> ( B x. ( Im ` ( F ` x ) ) ) ) )
31 27 30 eqtr4d 
 |-  ( ph -> ( x e. A |-> ( Im ` ( B x. ( F ` x ) ) ) ) = ( ( A X. { B } ) oF x. ( x e. A |-> ( Im ` ( F ` x ) ) ) ) )
32 21 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` ( F ` x ) ) ) e. MblFn )
33 28 fmpttd 
 |-  ( ph -> ( x e. A |-> ( Im ` ( F ` x ) ) ) : A --> RR )
34 32 2 33 mbfmulc2lem 
 |-  ( ph -> ( ( A X. { B } ) oF x. ( x e. A |-> ( Im ` ( F ` x ) ) ) ) e. MblFn )
35 31 34 eqeltrd 
 |-  ( ph -> ( x e. A |-> ( Im ` ( B x. ( F ` x ) ) ) ) e. MblFn )
36 2 recnd 
 |-  ( ph -> B e. CC )
37 36 adantr 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
38 37 8 mulcld 
 |-  ( ( ph /\ x e. A ) -> ( B x. ( F ` x ) ) e. CC )
39 38 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> ( B x. ( F ` x ) ) ) e. MblFn <-> ( ( x e. A |-> ( Re ` ( B x. ( F ` x ) ) ) ) e. MblFn /\ ( x e. A |-> ( Im ` ( B x. ( F ` x ) ) ) ) e. MblFn ) ) )
40 25 35 39 mpbir2and 
 |-  ( ph -> ( x e. A |-> ( B x. ( F ` x ) ) ) e. MblFn )
41 12 40 eqeltrd 
 |-  ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )