# 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 )`
` |-  ( ( ph /\ x e. A ) -> B e. RR )`
8 3 ffvelrnda
` |-  ( ( 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 )`
` |-  ( ( ph /\ x e. A ) -> B e. CC )`
` |-  ( ( ph /\ x e. A ) -> ( B x. ( F ` x ) ) e. CC )`
` |-  ( 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 ) ) )`
` |-  ( ph -> ( x e. A |-> ( B x. ( F ` x ) ) ) e. MblFn )`
` |-  ( ph -> ( ( A X. { B } ) oF x. F ) e. MblFn )`