Metamath Proof Explorer

Theorem mbfmul

Description: The product of two measurable functions is measurable. (Contributed by Mario Carneiro, 7-Sep-2014)

Ref Expression
Hypotheses mbfmul.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfmul.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
Assertion mbfmul ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfmul.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfmul.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
3 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
4 1 3 syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
5 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
6 mbff ⊢ ( 𝐺 ∈ MblFn → 𝐺 : dom 𝐺 ⟶ ℂ )
7 2 6 syl ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℂ )
8 7 ffnd ⊢ ( 𝜑 → 𝐺 Fn dom 𝐺 )
9 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
10 1 9 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
11 mbfdm ⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
12 2 11 syl ⊢ ( 𝜑 → dom 𝐺 ∈ dom vol )
13 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16 5 8 10 12 13 14 15 offval ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) )
17 elinel1 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐹 )
18 ffvelcdm ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
19 4 17 18 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
20 elinel2 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
21 ffvelcdm ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
22 7 20 21 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
23 19 22 remuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) = ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) − ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
24 23 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) − ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
25 inmbl ⊢ ( ( dom 𝐹 ∈ dom vol ∧ dom 𝐺 ∈ dom vol ) → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
26 10 12 25 syl2anc ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
27 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
28 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
29 19 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
30 22 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
31 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
32 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
33 26 29 30 31 32 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
34 19 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
35 22 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
36 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
37 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
38 26 34 35 36 37 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
39 26 27 28 33 38 offval2 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f − ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) − ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
40 24 39 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f − ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
41 inss1 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹
42 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
43 41 42 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) )
44 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) )
45 44 1 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
46 mbfres ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ∧ ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol ) → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
47 45 26 46 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
48 43 47 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
49 19 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) ) )
50 48 49 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) )
51 50 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
52 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
53 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
54 52 53 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) )
55 7 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) )
56 55 2 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
57 mbfres ⊢ ( ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn ∧ ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol ) → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
58 56 26 57 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
59 54 58 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
60 22 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ) ) )
61 59 60 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ) )
62 61 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
63 29 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
64 30 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
65 51 62 63 64 mbfmullem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
66 50 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
67 61 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
68 34 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
69 35 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
70 66 67 68 69 mbfmullem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
71 65 70 mbfsub ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f − ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ MblFn )
72 40 71 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
73 19 22 immuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) = ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) + ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
74 73 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) + ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
75 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
76 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ V )
77 26 29 35 31 37 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
78 26 34 30 36 32 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
79 26 75 76 77 78 offval2 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f + ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) + ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) · ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
80 74 79 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) = ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f + ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) )
81 51 67 63 69 mbfmullem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
82 66 62 68 64 mbfmullem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
83 81 82 mbfadd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∘f + ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ) ∈ MblFn )
84 80 83 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
85 19 22 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
86 85 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn ) ) )
87 72 84 86 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) · ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
88 16 87 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f · 𝐺 ) ∈ MblFn )