Step | Hyp | Ref
| Expression |
1 | | mbfadd.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ MblFn) |
2 | | mbff 23200 |
. . . . . . . 8
⊢ (𝐹 ∈ MblFn → 𝐹:dom 𝐹⟶ℂ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ) |
4 | | elin 3758 |
. . . . . . . 8
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↔ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺)) |
5 | 4 | simplbi 475 |
. . . . . . 7
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐹) |
6 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐹:dom 𝐹⟶ℂ ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ℂ) |
7 | 3, 5, 6 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐹‘𝑥) ∈ ℂ) |
8 | | mbfadd.2 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ MblFn) |
9 | | mbff 23200 |
. . . . . . . 8
⊢ (𝐺 ∈ MblFn → 𝐺:dom 𝐺⟶ℂ) |
10 | 8, 9 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺:dom 𝐺⟶ℂ) |
11 | 4 | simprbi 479 |
. . . . . . 7
⊢ (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) → 𝑥 ∈ dom 𝐺) |
12 | | ffvelrn 6265 |
. . . . . . 7
⊢ ((𝐺:dom 𝐺⟶ℂ ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) ∈ ℂ) |
13 | 10, 11, 12 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → (𝐺‘𝑥) ∈ ℂ) |
14 | 7, 13 | negsubd 10277 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) + -(𝐺‘𝑥)) = ((𝐹‘𝑥) − (𝐺‘𝑥))) |
15 | 14 | eqcomd 2616 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → ((𝐹‘𝑥) − (𝐺‘𝑥)) = ((𝐹‘𝑥) + -(𝐺‘𝑥))) |
16 | 15 | mpteq2dva 4672 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) − (𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + -(𝐺‘𝑥)))) |
17 | | ffn 5958 |
. . . . 5
⊢ (𝐹:dom 𝐹⟶ℂ → 𝐹 Fn dom 𝐹) |
18 | 3, 17 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
19 | | ffn 5958 |
. . . . 5
⊢ (𝐺:dom 𝐺⟶ℂ → 𝐺 Fn dom 𝐺) |
20 | 10, 19 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
21 | | mbfdm 23201 |
. . . . 5
⊢ (𝐹 ∈ MblFn → dom 𝐹 ∈ dom
vol) |
22 | 1, 21 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐹 ∈ dom vol) |
23 | | mbfdm 23201 |
. . . . 5
⊢ (𝐺 ∈ MblFn → dom 𝐺 ∈ dom
vol) |
24 | 8, 23 | syl 17 |
. . . 4
⊢ (𝜑 → dom 𝐺 ∈ dom vol) |
25 | | eqid 2610 |
. . . 4
⊢ (dom
𝐹 ∩ dom 𝐺) = (dom 𝐹 ∩ dom 𝐺) |
26 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) = (𝐹‘𝑥)) |
27 | | eqidd 2611 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ dom 𝐺) → (𝐺‘𝑥) = (𝐺‘𝑥)) |
28 | 18, 20, 22, 24, 25, 26, 27 | offval 6802 |
. . 3
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) − (𝐺‘𝑥)))) |
29 | | inmbl 23117 |
. . . . 5
⊢ ((dom
𝐹 ∈ dom vol ∧ dom
𝐺 ∈ dom vol) →
(dom 𝐹 ∩ dom 𝐺) ∈ dom
vol) |
30 | 22, 24, 29 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) |
31 | 13 | negcld 10258 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (dom 𝐹 ∩ dom 𝐺)) → -(𝐺‘𝑥) ∈ ℂ) |
32 | | eqidd 2611 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
33 | | eqidd 2611 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥))) |
34 | 30, 7, 31, 32, 33 | offval2 6812 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥))) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ ((𝐹‘𝑥) + -(𝐺‘𝑥)))) |
35 | 16, 28, 34 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) = ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥)))) |
36 | | inss1 3795 |
. . . . 5
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 |
37 | | resmpt 5369 |
. . . . 5
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐹 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
38 | 36, 37 | mp1i 13 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥))) |
39 | 3 | feqmptd 6159 |
. . . . . 6
⊢ (𝜑 → 𝐹 = (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥))) |
40 | 39, 1 | eqeltrrd 2689 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn) |
41 | | mbfres 23217 |
. . . . 5
⊢ (((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
42 | 40, 30, 41 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ↦ (𝐹‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
43 | 38, 42 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∈ MblFn) |
44 | | inss2 3796 |
. . . . . 6
⊢ (dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 |
45 | | resmpt 5369 |
. . . . . 6
⊢ ((dom
𝐹 ∩ dom 𝐺) ⊆ dom 𝐺 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
46 | 44, 45 | mp1i 13 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) = (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥))) |
47 | 10 | feqmptd 6159 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥))) |
48 | 47, 8 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn) |
49 | | mbfres 23217 |
. . . . . 6
⊢ (((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ∈ MblFn ∧ (dom 𝐹 ∩ dom 𝐺) ∈ dom vol) → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
50 | 48, 30, 49 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ dom 𝐺 ↦ (𝐺‘𝑥)) ↾ (dom 𝐹 ∩ dom 𝐺)) ∈ MblFn) |
51 | 46, 50 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐺‘𝑥)) ∈ MblFn) |
52 | 13, 51 | mbfneg 23223 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥)) ∈ MblFn) |
53 | 43, 52 | mbfadd 23234 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ (𝐹‘𝑥)) ∘𝑓 + (𝑥 ∈ (dom 𝐹 ∩ dom 𝐺) ↦ -(𝐺‘𝑥))) ∈ MblFn) |
54 | 35, 53 | eqeltrd 2688 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 − 𝐺) ∈ MblFn) |