Step | Hyp | Ref
| Expression |
1 | | mbfadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | mbff 23791 |
. . . . 5
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
4 | 3 | ffnd 6279 |
. . 3
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
5 | | mbfadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ MblFn) |
6 | | mbff 23791 |
. . . . 5
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
8 | 7 | ffnd 6279 |
. . 3
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
9 | | mbfdm 23792 |
. . . 4
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
10 | 1, 9 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
11 | | mbfdm 23792 |
. . . 4
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
12 | 5, 11 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
13 | | eqid 2825 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
14 | | eqidd 2826 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
15 | | eqidd 2826 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
16 | 4, 8, 10, 12, 13, 14, 15 | offval 7164 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
17 | | elin 4023 |
. . . . . . . . 9
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
18 | 17 | simplbi 493 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
19 | | ffvelrn 6606 |
. . . . . . . 8
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
20 | 3, 18, 19 | syl2an 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
21 | 17 | simprbi 492 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
22 | | ffvelrn 6606 |
. . . . . . . 8
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
23 | 7, 21, 22 | syl2an 591 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
24 | 20, 23 | readdd 14331 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥)))) |
25 | 24 | mpteq2dva 4967 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
26 | | inmbl 23708 |
. . . . . . 7
⊢ ((dom
𝐹 ∈ dom vol ∧ dom
𝐺 ∈ dom vol) →
(dom 𝐹 ∩ dom 𝐺) ∈ dom
vol) |
27 | 10, 12, 26 | syl2anc 581 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
28 | 20 | recld 14311 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
29 | 23 | recld 14311 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐺‘𝑥)) ∈ ℝ) |
30 | | eqidd 2826 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥)))) |
31 | | eqidd 2826 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) |
32 | 27, 28, 29, 30, 31 | offval2 7174 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
33 | 25, 32 | eqtr4d 2864 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))))) |
34 | | inss1 4057 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
35 | | resmpt 5686 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) |
37 | 3 | feqmptd 6496 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥))) |
38 | 37, 1 | eqeltrrd 2907 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn) |
39 | | mbfres 23810 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
40 | 38, 27, 39 | syl2anc 581 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
41 | 36, 40 | syl5eqelr 2911 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn) |
42 | 20 | ismbfcn2 23804 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn))) |
43 | 41, 42 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn)) |
44 | 43 | simpld 490 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
45 | | inss2 4058 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
46 | | resmpt 5686 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
47 | 45, 46 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) |
48 | 7 | feqmptd 6496 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
49 | 48, 5 | eqeltrrd 2907 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn) |
50 | | mbfres 23810 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
51 | 49, 27, 50 | syl2anc 581 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
52 | 47, 51 | syl5eqelr 2911 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn) |
53 | 23 | ismbfcn2 23804 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn))) |
54 | 52, 53 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn)) |
55 | 54 | simpld 490 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn) |
56 | 28 | fmpttd 6634 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
57 | 29 | fmpttd 6634 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
58 | 44, 55, 56, 57 | mbfaddlem 23826 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∈ MblFn) |
59 | 33, 58 | eqeltrd 2906 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
60 | 20, 23 | imaddd 14332 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥)))) |
61 | 60 | mpteq2dva 4967 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
62 | 20 | imcld 14312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐹‘𝑥)) ∈ ℝ) |
63 | 23 | imcld 14312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐺‘𝑥)) ∈ ℝ) |
64 | | eqidd 2826 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥)))) |
65 | | eqidd 2826 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) |
66 | 27, 62, 63, 64, 65 | offval2 7174 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
67 | 61, 66 | eqtr4d 2864 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))))) |
68 | 43 | simprd 491 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn) |
69 | 54 | simprd 491 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn) |
70 | 62 | fmpttd 6634 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
71 | 63 | fmpttd 6634 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
72 | 68, 69, 70, 71 | mbfaddlem 23826 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∈ MblFn) |
73 | 67, 72 | eqeltrd 2906 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
74 | 20, 23 | addcld 10376 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) + (𝐺‘𝑥)) ∈ ℂ) |
75 | 74 | ismbfcn2 23804 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn))) |
76 | 59, 73, 75 | mpbir2and 706 |
. 2
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn) |
77 | 16, 76 | eqeltrd 2906 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 + 𝐺) ∈ MblFn) |