# Metamath Proof Explorer

## Theorem mbfmulc2re

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

Ref Expression
Hypotheses mbfmulc2re.1 ${⊢}{\phi }\to {F}\in MblFn$
mbfmulc2re.2 ${⊢}{\phi }\to {B}\in ℝ$
mbfmulc2re.3 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
Assertion mbfmulc2re ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}{F}\in MblFn$

### Proof

Step Hyp Ref Expression
1 mbfmulc2re.1 ${⊢}{\phi }\to {F}\in MblFn$
2 mbfmulc2re.2 ${⊢}{\phi }\to {B}\in ℝ$
3 mbfmulc2re.3 ${⊢}{\phi }\to {F}:{A}⟶ℂ$
4 3 fdmd ${⊢}{\phi }\to \mathrm{dom}{F}={A}$
5 1 dmexd ${⊢}{\phi }\to \mathrm{dom}{F}\in \mathrm{V}$
6 4 5 eqeltrrd ${⊢}{\phi }\to {A}\in \mathrm{V}$
7 2 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℝ$
8 3 ffvelrnda ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {F}\left({x}\right)\in ℂ$
9 fconstmpt ${⊢}{A}×\left\{{B}\right\}=\left({x}\in {A}⟼{B}\right)$
10 9 a1i ${⊢}{\phi }\to {A}×\left\{{B}\right\}=\left({x}\in {A}⟼{B}\right)$
11 3 feqmptd ${⊢}{\phi }\to {F}=\left({x}\in {A}⟼{F}\left({x}\right)\right)$
12 6 7 8 10 11 offval2 ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}{F}=\left({x}\in {A}⟼{B}{F}\left({x}\right)\right)$
13 7 8 remul2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({B}{F}\left({x}\right)\right)={B}\Re \left({F}\left({x}\right)\right)$
14 13 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({B}{F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼{B}\Re \left({F}\left({x}\right)\right)\right)$
15 8 recld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({F}\left({x}\right)\right)\in ℝ$
16 eqidd ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)$
17 6 7 15 10 16 offval2 ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼{B}\Re \left({F}\left({x}\right)\right)\right)$
18 14 17 eqtr4d ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({B}{F}\left({x}\right)\right)\right)=\left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)$
19 11 1 eqeltrrd ${⊢}{\phi }\to \left({x}\in {A}⟼{F}\left({x}\right)\right)\in MblFn$
20 8 ismbfcn2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{F}\left({x}\right)\right)\in MblFn↔\left(\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)\in MblFn\right)\right)$
21 19 20 mpbid ${⊢}{\phi }\to \left(\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)\in MblFn\right)$
22 21 simpld ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)\in MblFn$
23 15 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right):{A}⟶ℝ$
24 22 2 23 mbfmulc2lem ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Re \left({F}\left({x}\right)\right)\right)\in MblFn$
25 18 24 eqeltrd ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({B}{F}\left({x}\right)\right)\right)\in MblFn$
26 7 8 immul2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({B}{F}\left({x}\right)\right)={B}\Im \left({F}\left({x}\right)\right)$
27 26 mpteq2dva ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({B}{F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼{B}\Im \left({F}\left({x}\right)\right)\right)$
28 8 imcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({F}\left({x}\right)\right)\in ℝ$
29 eqidd ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)$
30 6 7 28 10 29 offval2 ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)=\left({x}\in {A}⟼{B}\Im \left({F}\left({x}\right)\right)\right)$
31 27 30 eqtr4d ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({B}{F}\left({x}\right)\right)\right)=\left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)$
32 21 simprd ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)\in MblFn$
33 28 fmpttd ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right):{A}⟶ℝ$
34 32 2 33 mbfmulc2lem ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}\left({x}\in {A}⟼\Im \left({F}\left({x}\right)\right)\right)\in MblFn$
35 31 34 eqeltrd ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({B}{F}\left({x}\right)\right)\right)\in MblFn$
36 2 recnd ${⊢}{\phi }\to {B}\in ℂ$
37 36 adantr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
38 37 8 mulcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}{F}\left({x}\right)\in ℂ$
39 38 ismbfcn2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}{F}\left({x}\right)\right)\in MblFn↔\left(\left({x}\in {A}⟼\Re \left({B}{F}\left({x}\right)\right)\right)\in MblFn\wedge \left({x}\in {A}⟼\Im \left({B}{F}\left({x}\right)\right)\right)\in MblFn\right)\right)$
40 25 35 39 mpbir2and ${⊢}{\phi }\to \left({x}\in {A}⟼{B}{F}\left({x}\right)\right)\in MblFn$
41 12 40 eqeltrd ${⊢}{\phi }\to \left({A}×\left\{{B}\right\}\right){×}_{f}{F}\in MblFn$