Step | Hyp | Ref
| Expression |
1 | | mbfadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | mbff 23394 |
. . . . 5
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
4 | | ffn 6045 |
. . . 4
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
6 | | mbfadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ MblFn) |
7 | | mbff 23394 |
. . . . 5
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
9 | | ffn 6045 |
. . . 4
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
11 | | mbfdm 23395 |
. . . 4
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
12 | 1, 11 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
13 | | mbfdm 23395 |
. . . 4
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
14 | 6, 13 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
15 | | eqid 2622 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
16 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
17 | | eqidd 2623 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
18 | 5, 10, 12, 14, 15, 16, 17 | offval 6904 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
19 | | elin 3796 |
. . . . . . . . 9
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
20 | 19 | simplbi 476 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
21 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
22 | 3, 20, 21 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
23 | 19 | simprbi 480 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
24 | | ffvelrn 6357 |
. . . . . . . 8
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
25 | 8, 23, 24 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
26 | 22, 25 | readdd 13954 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥)))) |
27 | 26 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
28 | | inmbl 23310 |
. . . . . . 7
⊢ ((dom
𝐹 ∈ dom vol ∧ dom
𝐺 ∈ dom vol) →
(dom 𝐹 ∩ dom 𝐺) ∈ dom
vol) |
29 | 12, 14, 28 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
30 | 22 | recld 13934 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
31 | 25 | recld 13934 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐺‘𝑥)) ∈ ℝ) |
32 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥)))) |
33 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) |
34 | 29, 30, 31, 32, 33 | offval2 6914 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
35 | 27, 34 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))))) |
36 | | inss1 3833 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
37 | | resmpt 5449 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) |
39 | 3 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥))) |
40 | 39, 1 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn) |
41 | | mbfres 23411 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
42 | 40, 29, 41 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
43 | 38, 42 | syl5eqelr 2706 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn) |
44 | 22 | ismbfcn2 23406 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn))) |
45 | 43, 44 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn)) |
46 | 45 | simpld 475 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
47 | | inss2 3834 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
48 | | resmpt 5449 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
49 | 47, 48 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) |
50 | 8 | feqmptd 6249 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
51 | 50, 6 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn) |
52 | | mbfres 23411 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
53 | 51, 29, 52 | syl2anc 693 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
54 | 49, 53 | syl5eqelr 2706 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn) |
55 | 25 | ismbfcn2 23406 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn))) |
56 | 54, 55 | mpbid 222 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn)) |
57 | 56 | simpld 475 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn) |
58 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) |
59 | 30, 58 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
60 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) |
61 | 31, 60 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
62 | 46, 57, 59, 61 | mbfaddlem 23427 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∈ MblFn) |
63 | 35, 62 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
64 | 22, 25 | imaddd 13955 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥)))) |
65 | 64 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
66 | 22 | imcld 13935 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐹‘𝑥)) ∈ ℝ) |
67 | 25 | imcld 13935 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐺‘𝑥)) ∈ ℝ) |
68 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥)))) |
69 | | eqidd 2623 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) |
70 | 29, 66, 67, 68, 69 | offval2 6914 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
71 | 65, 70 | eqtr4d 2659 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))))) |
72 | 45 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn) |
73 | 56 | simprd 479 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn) |
74 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) |
75 | 66, 74 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
76 | | eqid 2622 |
. . . . . 6
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) |
77 | 67, 76 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
78 | 72, 73, 75, 77 | mbfaddlem 23427 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∈ MblFn) |
79 | 71, 78 | eqeltrd 2701 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
80 | 22, 25 | addcld 10059 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) + (𝐺‘𝑥)) ∈ ℂ) |
81 | 80 | ismbfcn2 23406 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn))) |
82 | 63, 79, 81 | mpbir2and 957 |
. 2
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn) |
83 | 18, 82 | eqeltrd 2701 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) |