# Metamath Proof Explorer

## Theorem mbfmulc2re

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

Ref Expression
Hypotheses mbfmulc2re.1 ( 𝜑𝐹 ∈ MblFn )
mbfmulc2re.2 ( 𝜑𝐵 ∈ ℝ )
mbfmulc2re.3 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
Assertion mbfmulc2re ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )

### Proof

Step Hyp Ref Expression
1 mbfmulc2re.1 ( 𝜑𝐹 ∈ MblFn )
2 mbfmulc2re.2 ( 𝜑𝐵 ∈ ℝ )
3 mbfmulc2re.3 ( 𝜑𝐹 : 𝐴 ⟶ ℂ )
4 3 fdmd ( 𝜑 → dom 𝐹 = 𝐴 )
5 1 dmexd ( 𝜑 → dom 𝐹 ∈ V )
6 4 5 eqeltrrd ( 𝜑𝐴 ∈ V )
7 2 adantr ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
8 3 ffvelrnda ( ( 𝜑𝑥𝐴 ) → ( 𝐹𝑥 ) ∈ ℂ )
9 fconstmpt ( 𝐴 × { 𝐵 } ) = ( 𝑥𝐴𝐵 )
10 9 a1i ( 𝜑 → ( 𝐴 × { 𝐵 } ) = ( 𝑥𝐴𝐵 ) )
11 3 feqmptd ( 𝜑𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
12 6 7 8 10 11 offval2 ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) = ( 𝑥𝐴 ↦ ( 𝐵 · ( 𝐹𝑥 ) ) ) )
13 7 8 remul2d ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) = ( 𝐵 · ( ℜ ‘ ( 𝐹𝑥 ) ) ) )
14 13 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 · ( ℜ ‘ ( 𝐹𝑥 ) ) ) ) )
15 8 recld ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
16 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) = ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) )
17 6 7 15 10 16 offval2 ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 · ( ℜ ‘ ( 𝐹𝑥 ) ) ) ) )
18 14 17 eqtr4d ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) = ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ) )
19 11 1 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ∈ MblFn )
20 8 ismbfcn2 ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn ) ) )
21 19 20 mpbid ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn ) )
22 21 simpld ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn )
23 15 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) : 𝐴 ⟶ ℝ )
24 22 2 23 mbfmulc2lem ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐹𝑥 ) ) ) ) ∈ MblFn )
25 18 24 eqeltrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) ∈ MblFn )
26 7 8 immul2d ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) = ( 𝐵 · ( ℑ ‘ ( 𝐹𝑥 ) ) ) )
27 26 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 · ( ℑ ‘ ( 𝐹𝑥 ) ) ) ) )
28 8 imcld ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ ( 𝐹𝑥 ) ) ∈ ℝ )
29 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) = ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) )
30 6 7 28 10 29 offval2 ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ) = ( 𝑥𝐴 ↦ ( 𝐵 · ( ℑ ‘ ( 𝐹𝑥 ) ) ) ) )
31 27 30 eqtr4d ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) = ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ) )
32 21 simprd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ∈ MblFn )
33 28 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) : 𝐴 ⟶ ℝ )
34 32 2 33 mbfmulc2lem ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐹𝑥 ) ) ) ) ∈ MblFn )
35 31 34 eqeltrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) ∈ MblFn )
36 2 recnd ( 𝜑𝐵 ∈ ℂ )
37 36 adantr ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
38 37 8 mulcld ( ( 𝜑𝑥𝐴 ) → ( 𝐵 · ( 𝐹𝑥 ) ) ∈ ℂ )
39 38 ismbfcn2 ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐵 · ( 𝐹𝑥 ) ) ) ∈ MblFn ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) ∈ MblFn ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐵 · ( 𝐹𝑥 ) ) ) ) ∈ MblFn ) ) )
40 25 35 39 mpbir2and ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐵 · ( 𝐹𝑥 ) ) ) ∈ MblFn )
41 12 40 eqeltrd ( 𝜑 → ( ( 𝐴 × { 𝐵 } ) ∘f · 𝐹 ) ∈ MblFn )