Step | Hyp | Ref
| Expression |
1 | | mbfmul.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | mbff 23732 |
. . . . 5
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
4 | 3 | ffnd 6258 |
. . 3
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
5 | | mbfmul.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ MblFn) |
6 | | mbff 23732 |
. . . . 5
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
8 | 7 | ffnd 6258 |
. . 3
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
9 | | mbfdm 23733 |
. . . 4
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
10 | 1, 9 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
11 | | mbfdm 23733 |
. . . 4
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
12 | 5, 11 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
13 | | eqid 2800 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
14 | | eqidd 2801 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | | eqidd 2801 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
16 | 4, 8, 10, 12, 13, 14, 15 | offval 7139 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥)))) |
17 | | elin 3995 |
. . . . . . . . 9
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
18 | 17 | simplbi 492 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
19 | | ffvelrn 6584 |
. . . . . . . 8
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
20 | 3, 18, 19 | syl2an 590 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
21 | 17 | simprbi 491 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
22 | | ffvelrn 6584 |
. . . . . . . 8
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
23 | 7, 21, 22 | syl2an 590 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
24 | 20, 23 | remuld 14298 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘((𝐹‘𝑥) · (𝐺‘𝑥))) = (((ℜ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))) − ((ℑ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))))) |
25 | 24 | mpteq2dva 4938 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (((ℜ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))) − ((ℑ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥)))))) |
26 | | inmbl 23649 |
. . . . . . 7
⊢ ((dom
𝐹 ∈ dom vol ∧ dom
𝐺 ∈ dom vol) →
(dom 𝐹 ∩ dom 𝐺) ∈ dom
vol) |
27 | 10, 12, 26 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
28 | | ovexd 6913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((ℜ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))) ∈ V) |
29 | | ovexd 6913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((ℑ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))) ∈ V) |
30 | 20 | recld 14274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
31 | 23 | recld 14274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐺‘𝑥)) ∈ ℝ) |
32 | | eqidd 2801 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥)))) |
33 | | eqidd 2801 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) |
34 | 27, 30, 31, 32, 33 | offval2 7149 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))))) |
35 | 20 | imcld 14275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐹‘𝑥)) ∈ ℝ) |
36 | 23 | imcld 14275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐺‘𝑥)) ∈ ℝ) |
37 | | eqidd 2801 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥)))) |
38 | | eqidd 2801 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) |
39 | 27, 35, 36, 37, 38 | offval2 7149 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))))) |
40 | 27, 28, 29, 34, 39 | offval2 7149 |
. . . . 5
⊢ (𝜑 → (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∘𝑓 −
((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (((ℜ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))) − ((ℑ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥)))))) |
41 | 25, 40 | eqtr4d 2837 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) = (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∘𝑓 −
((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))))) |
42 | | inss1 4029 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
43 | | resmpt 5662 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) |
45 | 3 | feqmptd 6475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 = (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥))) |
46 | 45, 1 | eqeltrrd 2880 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn) |
47 | | mbfres 23751 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
48 | 46, 27, 47 | syl2anc 580 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
49 | 44, 48 | syl5eqelr 2884 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn) |
50 | 20 | ismbfcn2 23745 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn))) |
51 | 49, 50 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn)) |
52 | 51 | simpld 489 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
53 | | inss2 4030 |
. . . . . . . . . 10
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
54 | | resmpt 5662 |
. . . . . . . . . 10
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
⊢ ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) |
56 | 7 | feqmptd 6475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
57 | 56, 5 | eqeltrrd 2880 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn) |
58 | | mbfres 23751 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
59 | 57, 27, 58 | syl2anc 580 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
60 | 55, 59 | syl5eqelr 2884 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn) |
61 | 23 | ismbfcn2 23745 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn))) |
62 | 60, 61 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn)) |
63 | 62 | simpld 489 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn) |
64 | 30 | fmpttd 6612 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
65 | 31 | fmpttd 6612 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
66 | 52, 63, 64, 65 | mbfmullem 23832 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∈ MblFn) |
67 | 51 | simprd 490 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn) |
68 | 62 | simprd 490 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn) |
69 | 35 | fmpttd 6612 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
70 | 36 | fmpttd 6612 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
71 | 67, 68, 69, 70 | mbfmullem 23832 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∈ MblFn) |
72 | 66, 71 | mbfsub 23769 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∘𝑓 −
((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))))) ∈ MblFn) |
73 | 41, 72 | eqeltrd 2879 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) ∈ MblFn) |
74 | 20, 23 | immuld 14299 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘((𝐹‘𝑥) · (𝐺‘𝑥))) = (((ℜ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))) + ((ℑ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))))) |
75 | 74 | mpteq2dva 4938 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (((ℜ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))) + ((ℑ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥)))))) |
76 | | ovexd 6913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((ℜ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))) ∈ V) |
77 | | ovexd 6913 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((ℑ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))) ∈ V) |
78 | 27, 30, 36, 32, 38 | offval2 7149 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))))) |
79 | 27, 35, 31, 37, 33 | offval2 7149 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥))))) |
80 | 27, 76, 77, 78, 79 | offval2 7149 |
. . . . 5
⊢ (𝜑 → (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∘𝑓 + ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (((ℜ‘(𝐹‘𝑥)) · (ℑ‘(𝐺‘𝑥))) + ((ℑ‘(𝐹‘𝑥)) · (ℜ‘(𝐺‘𝑥)))))) |
81 | 75, 80 | eqtr4d 2837 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) = (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∘𝑓 + ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))))) |
82 | 52, 68, 64, 70 | mbfmullem 23832 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∈ MblFn) |
83 | 67, 63, 69, 65 | mbfmullem 23832 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∈ MblFn) |
84 | 82, 83 | mbfadd 23768 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∘𝑓 + ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))))) ∈ MblFn) |
85 | 81, 84 | eqeltrd 2879 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) ∈ MblFn) |
86 | 20, 23 | mulcld 10350 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) · (𝐺‘𝑥)) ∈ ℂ) |
87 | 86 | ismbfcn2 23745 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) · (𝐺‘𝑥)))) ∈ MblFn))) |
88 | 73, 85, 87 | mpbir2and 705 |
. 2
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) · (𝐺‘𝑥))) ∈ MblFn) |
89 | 16, 88 | eqeltrd 2879 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 · 𝐺) ∈ MblFn) |