Metamath Proof Explorer

Theorem mbfadd

Description: The sum of two measurable functions is measurable. (Contributed by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses mbfadd.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfadd.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
Assertion mbfadd ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ MblFn )

Proof

Step Hyp Ref Expression
1 mbfadd.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
2 mbfadd.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
3 mbff ⊢ ( 𝐹 ∈ MblFn → 𝐹 : dom 𝐹 ⟶ ℂ )
4 1 3 syl ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
5 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
6 mbff ⊢ ( 𝐺 ∈ MblFn → 𝐺 : dom 𝐺 ⟶ ℂ )
7 2 6 syl ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℂ )
8 7 ffnd ⊢ ( 𝜑 → 𝐺 Fn dom 𝐺 )
9 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
10 1 9 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
11 mbfdm ⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
12 2 11 syl ⊢ ( 𝜑 → dom 𝐺 ∈ dom vol )
13 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
15 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
16 5 8 10 12 13 14 15 offval ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) )
17 elinel1 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐹 )
18 ffvelrn ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
19 4 17 18 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
20 elinel2 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
21 ffvelrn ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
22 7 20 21 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
23 19 22 readdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) = ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
24 23 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
25 inmbl ⊢ ( ( dom 𝐹 ∈ dom vol ∧ dom 𝐺 ∈ dom vol ) → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
26 10 12 25 syl2anc ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
27 19 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
28 22 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
29 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
30 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
31 26 27 28 29 30 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
32 24 31 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) = ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
33 inss1 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹
34 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
35 33 34 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) )
36 4 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) )
37 36 1 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
38 mbfres ⊢ ( ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ∧ ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol ) → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
39 37 26 38 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
40 35 39 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
41 19 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) ) )
42 40 41 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn ) )
43 42 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
44 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
45 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
46 44 45 ax-mp ⊢ ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) )
47 7 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) )
48 47 2 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
49 mbfres ⊢ ( ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn ∧ ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol ) → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
50 48 26 49 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
51 46 50 eqeltrrid ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
52 22 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ) ) )
53 51 52 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ) )
54 53 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
55 27 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
56 28 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
57 43 54 55 56 mbfaddlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
58 32 57 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
59 19 22 imaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) = ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
60 59 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
61 19 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ )
62 22 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ℝ )
63 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
64 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) )
65 26 61 62 63 64 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) + ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
66 60 65 eqtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) = ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) )
67 42 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ MblFn )
68 53 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
69 61 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
70 62 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) : ( dom 𝐹 ∩ dom 𝐺 ) ⟶ ℝ )
71 67 68 69 70 mbfaddlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
72 66 71 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn )
73 19 22 addcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
74 73 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn ↔ ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℜ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn ∧ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ℑ ‘ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ MblFn ) ) )
75 58 72 74 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
76 16 75 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f + 𝐺 ) ∈ MblFn )