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 
|- ( ph -> F e. MblFn )
mbfadd.2 
|- ( ph -> G e. MblFn )
Assertion mbfsub 
|- ( ph -> ( F oF - G ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfadd.1 
 |-  ( ph -> F e. MblFn )
2 mbfadd.2 
 |-  ( ph -> G e. MblFn )
3 mbff 
 |-  ( F e. MblFn -> F : dom F --> CC )
4 1 3 syl 
 |-  ( ph -> F : dom F --> CC )
5 elinel1 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom F )
6 ffvelcdm 
 |-  ( ( F : dom F --> CC /\ x e. dom F ) -> ( F ` x ) e. CC )
7 4 5 6 syl2an 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( F ` x ) e. CC )
8 mbff 
 |-  ( G e. MblFn -> G : dom G --> CC )
9 2 8 syl 
 |-  ( ph -> G : dom G --> CC )
10 elinel2 
 |-  ( x e. ( dom F i^i dom G ) -> x e. dom G )
11 ffvelcdm 
 |-  ( ( G : dom G --> CC /\ x e. dom G ) -> ( G ` x ) e. CC )
12 9 10 11 syl2an 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( G ` x ) e. CC )
13 7 12 negsubd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( F ` x ) + -u ( G ` x ) ) = ( ( F ` x ) - ( G ` x ) ) )
14 13 eqcomd 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> ( ( F ` x ) - ( G ` x ) ) = ( ( F ` x ) + -u ( G ` x ) ) )
15 14 mpteq2dva 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) - ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + -u ( G ` x ) ) ) )
16 4 ffnd 
 |-  ( ph -> F Fn dom F )
17 9 ffnd 
 |-  ( ph -> G Fn dom G )
18 mbfdm 
 |-  ( F e. MblFn -> dom F e. dom vol )
19 1 18 syl 
 |-  ( ph -> dom F e. dom vol )
20 mbfdm 
 |-  ( G e. MblFn -> dom G e. dom vol )
21 2 20 syl 
 |-  ( ph -> dom G e. dom vol )
22 eqid 
 |-  ( dom F i^i dom G ) = ( dom F i^i dom G )
23 eqidd 
 |-  ( ( ph /\ x e. dom F ) -> ( F ` x ) = ( F ` x ) )
24 eqidd 
 |-  ( ( ph /\ x e. dom G ) -> ( G ` x ) = ( G ` x ) )
25 16 17 19 21 22 23 24 offval 
 |-  ( ph -> ( F oF - G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) - ( G ` x ) ) ) )
26 inmbl 
 |-  ( ( dom F e. dom vol /\ dom G e. dom vol ) -> ( dom F i^i dom G ) e. dom vol )
27 19 21 26 syl2anc 
 |-  ( ph -> ( dom F i^i dom G ) e. dom vol )
28 12 negcld 
 |-  ( ( ph /\ x e. ( dom F i^i dom G ) ) -> -u ( G ` x ) e. CC )
29 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) )
30 eqidd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) = ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) )
31 27 7 28 29 30 offval2 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) oF + ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) + -u ( G ` x ) ) ) )
32 15 25 31 3eqtr4d 
 |-  ( ph -> ( F oF - G ) = ( ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) oF + ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) ) )
33 inss1 
 |-  ( dom F i^i dom G ) C_ dom F
34 resmpt 
 |-  ( ( dom F i^i dom G ) C_ dom F -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) )
35 33 34 mp1i 
 |-  ( ph -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) )
36 4 feqmptd 
 |-  ( ph -> F = ( x e. dom F |-> ( F ` x ) ) )
37 36 1 eqeltrrd 
 |-  ( ph -> ( x e. dom F |-> ( F ` x ) ) e. MblFn )
38 mbfres 
 |-  ( ( ( x e. dom F |-> ( F ` x ) ) e. MblFn /\ ( dom F i^i dom G ) e. dom vol ) -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
39 37 27 38 syl2anc 
 |-  ( ph -> ( ( x e. dom F |-> ( F ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
40 35 39 eqeltrrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) e. MblFn )
41 inss2 
 |-  ( dom F i^i dom G ) C_ dom G
42 resmpt 
 |-  ( ( dom F i^i dom G ) C_ dom G -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) )
43 41 42 mp1i 
 |-  ( ph -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) = ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) )
44 9 feqmptd 
 |-  ( ph -> G = ( x e. dom G |-> ( G ` x ) ) )
45 44 2 eqeltrrd 
 |-  ( ph -> ( x e. dom G |-> ( G ` x ) ) e. MblFn )
46 mbfres 
 |-  ( ( ( x e. dom G |-> ( G ` x ) ) e. MblFn /\ ( dom F i^i dom G ) e. dom vol ) -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
47 45 27 46 syl2anc 
 |-  ( ph -> ( ( x e. dom G |-> ( G ` x ) ) |` ( dom F i^i dom G ) ) e. MblFn )
48 43 47 eqeltrrd 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> ( G ` x ) ) e. MblFn )
49 12 48 mbfneg 
 |-  ( ph -> ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) e. MblFn )
50 40 49 mbfadd 
 |-  ( ph -> ( ( x e. ( dom F i^i dom G ) |-> ( F ` x ) ) oF + ( x e. ( dom F i^i dom G ) |-> -u ( G ` x ) ) ) e. MblFn )
51 32 50 eqeltrd 
 |-  ( ph -> ( F oF - G ) e. MblFn )