| Step | Hyp | Ref
| Expression |
| 1 | | mbfadd.1 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ MblFn) |
| 2 | | mbff 25660 |
. . . . 5
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
| 3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
| 4 | 3 | ffnd 6737 |
. . 3
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
| 5 | | mbfadd.2 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ MblFn) |
| 6 | | mbff 25660 |
. . . . 5
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
| 8 | 7 | ffnd 6737 |
. . 3
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
| 9 | | mbfdm 25661 |
. . . 4
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
| 10 | 1, 9 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
| 11 | | mbfdm 25661 |
. . . 4
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
| 12 | 5, 11 | syl 17 |
. . 3
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
| 13 | | eqid 2737 |
. . 3
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
| 14 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
| 15 | | eqidd 2738 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
| 16 | 4, 8, 10, 12, 13, 14, 15 | offval 7706 |
. 2
⊢ (𝜑 → (𝐹 ∘f + 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥)))) |
| 17 | | elinel1 4201 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
| 18 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
| 19 | 3, 17, 18 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
| 20 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
| 21 | | ffvelcdm 7101 |
. . . . . . . 8
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
| 22 | 7, 20, 21 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
| 23 | 19, 22 | readdd 15253 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥)))) |
| 24 | 23 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
| 25 | | inmbl 25577 |
. . . . . . 7
⊢ ((dom
𝐹 ∈ dom vol ∧ dom
𝐺 ∈ dom vol) →
(dom 𝐹 ∩ dom 𝐺) ∈ dom
vol) |
| 26 | 10, 12, 25 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
| 27 | 19 | recld 15233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐹‘𝑥)) ∈ ℝ) |
| 28 | 22 | recld 15233 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℜ‘(𝐺‘𝑥)) ∈ ℝ) |
| 29 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥)))) |
| 30 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) |
| 31 | 26, 27, 28, 29, 30 | offval2 7717 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℜ‘(𝐹‘𝑥)) + (ℜ‘(𝐺‘𝑥))))) |
| 32 | 24, 31 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))))) |
| 33 | | inss1 4237 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
| 34 | | resmpt 6055 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
| 35 | 33, 34 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) |
| 36 | 3 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 = (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥))) |
| 37 | 36, 1 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn) |
| 38 | | mbfres 25679 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
| 39 | 37, 26, 38 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
| 40 | 35, 39 | eqeltrrid 2846 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn) |
| 41 | 19 | ismbfcn2 25673 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn))) |
| 42 | 40, 41 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn)) |
| 43 | 42 | simpld 494 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∈ MblFn) |
| 44 | | inss2 4238 |
. . . . . . . . 9
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
| 45 | | resmpt 6055 |
. . . . . . . . 9
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
| 46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) |
| 47 | 7 | feqmptd 6977 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
| 48 | 47, 5 | eqeltrrd 2842 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn) |
| 49 | | mbfres 25679 |
. . . . . . . . 9
⊢ (((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
| 50 | 48, 26, 49 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
| 51 | 46, 50 | eqeltrrid 2846 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn) |
| 52 | 22 | ismbfcn2 25673 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn))) |
| 53 | 51, 52 | mpbid 232 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn)) |
| 54 | 53 | simpld 494 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))) ∈ MblFn) |
| 55 | 27 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
| 56 | 28 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
| 57 | 43, 54, 55, 56 | mbfaddlem 25695 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘(𝐺‘𝑥)))) ∈ MblFn) |
| 58 | 32, 57 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
| 59 | 19, 22 | imaddd 15254 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥))) = ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥)))) |
| 60 | 59 | mpteq2dva 5242 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
| 61 | 19 | imcld 15234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐹‘𝑥)) ∈ ℝ) |
| 62 | 22 | imcld 15234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (ℑ‘(𝐺‘𝑥)) ∈ ℝ) |
| 63 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥)))) |
| 64 | | eqidd 2738 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) |
| 65 | 26, 61, 62, 63, 64 | offval2 7717 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((ℑ‘(𝐹‘𝑥)) + (ℑ‘(𝐺‘𝑥))))) |
| 66 | 60, 65 | eqtr4d 2780 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))))) |
| 67 | 42 | simprd 495 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∈ MblFn) |
| 68 | 53 | simprd 495 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))) ∈ MblFn) |
| 69 | 61 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
| 70 | 62 | fmpttd 7135 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥))):(dom 𝐹 ∩ dom 𝐺)⟶ℝ) |
| 71 | 67, 68, 69, 70 | mbfaddlem 25695 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐹‘𝑥))) ∘f + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘(𝐺‘𝑥)))) ∈ MblFn) |
| 72 | 66, 71 | eqeltrd 2841 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn) |
| 73 | 19, 22 | addcld 11280 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) + (𝐺‘𝑥)) ∈ ℂ) |
| 74 | 73 | ismbfcn2 25673 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn ↔ ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℜ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn ∧ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (ℑ‘((𝐹‘𝑥) + (𝐺‘𝑥)))) ∈ MblFn))) |
| 75 | 58, 72, 74 | mpbir2and 713 |
. 2
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + (𝐺‘𝑥))) ∈ MblFn) |
| 76 | 16, 75 | eqeltrd 2841 |
1
⊢ (𝜑 → (𝐹 ∘f + 𝐺) ∈ MblFn) |