Metamath Proof Explorer

Theorem mbfsub

Description: The difference of two measurable functions is measurable. (Contributed by Mario Carneiro, 5-Sep-2014)

Ref Expression
Hypotheses mbfadd.1 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
mbfadd.2 ⊢ ( 𝜑 → 𝐺 ∈ MblFn )
Assertion mbfsub ( 𝜑 → ( 𝐹 ∘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 elinel1 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐹 )
6 ffvelrn ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
7 4 5 6 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
8 mbff ⊢ ( 𝐺 ∈ MblFn → 𝐺 : dom 𝐺 ⟶ ℂ )
9 2 8 syl ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℂ )
10 elinel2 ⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
11 ffvelrn ⊢ ( ( 𝐺 : dom 𝐺 ⟶ ℂ ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
12 9 10 11 syl2an ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
13 7 12 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
14 13 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) )
15 14 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) ) )
16 4 ffnd ⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
17 9 ffnd ⊢ ( 𝜑 → 𝐺 Fn dom 𝐺 )
18 mbfdm ⊢ ( 𝐹 ∈ MblFn → dom 𝐹 ∈ dom vol )
19 1 18 syl ⊢ ( 𝜑 → dom 𝐹 ∈ dom vol )
20 mbfdm ⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
21 2 20 syl ⊢ ( 𝜑 → dom 𝐺 ∈ dom vol )
22 eqid ⊢ ( dom 𝐹 ∩ dom 𝐺 ) = ( dom 𝐹 ∩ dom 𝐺 )
23 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
24 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
25 16 17 19 21 22 23 24 offval ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
26 inmbl ⊢ ( ( dom 𝐹 ∈ dom vol ∧ dom 𝐺 ∈ dom vol ) → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
27 19 21 26 syl2anc ⊢ ( 𝜑 → ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol )
28 12 negcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ) → - ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
29 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
30 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) )
31 27 7 28 29 30 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( ( 𝐹 ‘ 𝑥 ) + - ( 𝐺 ‘ 𝑥 ) ) ) )
32 15 25 31 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) = ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) ) )
33 inss1 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹
34 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐹 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) )
35 33 34 mp1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 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 27 38 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ↦ ( 𝐹 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
40 35 39 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
41 inss2 ⊢ ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺
42 resmpt ⊢ ( ( dom 𝐹 ∩ dom 𝐺 ) ⊆ dom 𝐺 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
43 41 42 mp1i ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) = ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) )
44 9 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) )
45 44 2 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
46 mbfres ⊢ ( ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn ∧ ( dom 𝐹 ∩ dom 𝐺 ) ∈ dom vol ) → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
47 45 27 46 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐺 ↦ ( 𝐺 ‘ 𝑥 ) ) ↾ ( dom 𝐹 ∩ dom 𝐺 ) ) ∈ MblFn )
48 43 47 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
49 12 48 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) ∈ MblFn )
50 40 49 mbfadd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ ( 𝐹 ‘ 𝑥 ) ) ∘f + ( 𝑥 ∈ ( dom 𝐹 ∩ dom 𝐺 ) ↦ - ( 𝐺 ‘ 𝑥 ) ) ) ∈ MblFn )
51 32 50 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ∘f − 𝐺 ) ∈ MblFn )