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 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
mbfmulc2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
mbfmulc2.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
Assertion mbfmulc2 ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfmulc2.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 mbfmulc2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 mbfmulc2.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
4 3 2 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
5 1 recld ⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℝ )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
7 6 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
8 3 2 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9 8 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
10 9 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
11 7 10 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
12 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ V )
13 fconstmpt ⊢ ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) )
14 13 a1i ⊢ ( 𝜑 → ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) )
15 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
16 4 6 9 14 15 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
17 1 imcld ⊢ ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℝ )
18 17 renegcld ⊢ ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
20 8 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
21 fconstmpt ⊢ ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) )
22 21 a1i ⊢ ( 𝜑 → ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) ) )
23 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
24 4 19 20 22 23 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
25 4 11 12 16 24 offval2 ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
26 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
27 26 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
28 20 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
29 27 28 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
30 11 29 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
31 27 28 mulneg1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) = - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) )
32 31 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
33 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
34 33 8 remuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
35 30 32 34 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) = ( ℜ ‘ ( 𝐶 · 𝐵 ) ) )
36 35 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) + ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
37 25 36 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
38 8 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
39 3 38 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
40 39 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
41 10 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
42 40 5 41 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
43 39 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
44 28 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
45 43 18 44 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
46 42 45 mbfadd ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ) ∈ MblFn )
47 37 46 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
48 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ V )
49 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ V )
50 4 6 20 14 23 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
51 fconstmpt ⊢ ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) )
52 51 a1i ⊢ ( 𝜑 → ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) )
53 4 26 9 52 15 offval2 ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
54 4 48 49 50 53 offval2 ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
55 33 8 immuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
56 55 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
57 54 56 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) )
58 43 5 44 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
59 40 17 41 mbfmulc2re ⊢ ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
60 58 59 mbfadd ⊢ ( 𝜑 → ( ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∘f + ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ) ∈ MblFn )
61 57 60 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
62 33 8 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
63 62 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
64 47 61 63 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )