Metamath Proof Explorer

Theorem mbfres2

Description: Measurability of a piecewise function: if F is measurable on subsets B and C of its domain, and these pieces make up all of A , then F is measurable on the whole domain. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Hypotheses mbfres2.1 
|- ( ph -> F : A --> RR )
mbfres2.2 
|- ( ph -> ( F |` B ) e. MblFn )
mbfres2.3 
|- ( ph -> ( F |` C ) e. MblFn )
mbfres2.4 
|- ( ph -> ( B u. C ) = A )
Assertion mbfres2 
|- ( ph -> F e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfres2.1 
 |-  ( ph -> F : A --> RR )
2 mbfres2.2 
 |-  ( ph -> ( F |` B ) e. MblFn )
3 mbfres2.3 
 |-  ( ph -> ( F |` C ) e. MblFn )
4 mbfres2.4 
 |-  ( ph -> ( B u. C ) = A )
5 4 reseq2d 
 |-  ( ph -> ( F |` ( B u. C ) ) = ( F |` A ) )
6 ffn 
 |-  ( F : A --> RR -> F Fn A )
7 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
8 1 6 7 3syl 
 |-  ( ph -> ( F |` A ) = F )
9 5 8 eqtr2d 
 |-  ( ph -> F = ( F |` ( B u. C ) ) )
10 9 adantr 
 |-  ( ( ph /\ x e. ran (,) ) -> F = ( F |` ( B u. C ) ) )
11 resundi 
 |-  ( F |` ( B u. C ) ) = ( ( F |` B ) u. ( F |` C ) )
12 10 11 eqtrdi 
 |-  ( ( ph /\ x e. ran (,) ) -> F = ( ( F |` B ) u. ( F |` C ) ) )
13 12 cnveqd 
 |-  ( ( ph /\ x e. ran (,) ) -> `' F = `' ( ( F |` B ) u. ( F |` C ) ) )
14 cnvun 
 |-  `' ( ( F |` B ) u. ( F |` C ) ) = ( `' ( F |` B ) u. `' ( F |` C ) )
15 13 14 eqtrdi 
 |-  ( ( ph /\ x e. ran (,) ) -> `' F = ( `' ( F |` B ) u. `' ( F |` C ) ) )
16 15 imaeq1d 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' F " x ) = ( ( `' ( F |` B ) u. `' ( F |` C ) ) " x ) )
17 imaundir 
 |-  ( ( `' ( F |` B ) u. `' ( F |` C ) ) " x ) = ( ( `' ( F |` B ) " x ) u. ( `' ( F |` C ) " x ) )
18 16 17 eqtrdi 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' F " x ) = ( ( `' ( F |` B ) " x ) u. ( `' ( F |` C ) " x ) ) )
19 ssun1 
 |-  B C_ ( B u. C )
20 19 4 sseqtrid 
 |-  ( ph -> B C_ A )
21 1 20 fssresd 
 |-  ( ph -> ( F |` B ) : B --> RR )
22 ismbf 
 |-  ( ( F |` B ) : B --> RR -> ( ( F |` B ) e. MblFn <-> A. x e. ran (,) ( `' ( F |` B ) " x ) e. dom vol ) )
23 21 22 syl 
 |-  ( ph -> ( ( F |` B ) e. MblFn <-> A. x e. ran (,) ( `' ( F |` B ) " x ) e. dom vol ) )
24 2 23 mpbid 
 |-  ( ph -> A. x e. ran (,) ( `' ( F |` B ) " x ) e. dom vol )
25 24 r19.21bi 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' ( F |` B ) " x ) e. dom vol )
26 ssun2 
 |-  C C_ ( B u. C )
27 26 4 sseqtrid 
 |-  ( ph -> C C_ A )
28 1 27 fssresd 
 |-  ( ph -> ( F |` C ) : C --> RR )
29 ismbf 
 |-  ( ( F |` C ) : C --> RR -> ( ( F |` C ) e. MblFn <-> A. x e. ran (,) ( `' ( F |` C ) " x ) e. dom vol ) )
30 28 29 syl 
 |-  ( ph -> ( ( F |` C ) e. MblFn <-> A. x e. ran (,) ( `' ( F |` C ) " x ) e. dom vol ) )
31 3 30 mpbid 
 |-  ( ph -> A. x e. ran (,) ( `' ( F |` C ) " x ) e. dom vol )
32 31 r19.21bi 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' ( F |` C ) " x ) e. dom vol )
33 unmbl 
 |-  ( ( ( `' ( F |` B ) " x ) e. dom vol /\ ( `' ( F |` C ) " x ) e. dom vol ) -> ( ( `' ( F |` B ) " x ) u. ( `' ( F |` C ) " x ) ) e. dom vol )
34 25 32 33 syl2anc 
 |-  ( ( ph /\ x e. ran (,) ) -> ( ( `' ( F |` B ) " x ) u. ( `' ( F |` C ) " x ) ) e. dom vol )
35 18 34 eqeltrd 
 |-  ( ( ph /\ x e. ran (,) ) -> ( `' F " x ) e. dom vol )
36 35 ralrimiva 
 |-  ( ph -> A. x e. ran (,) ( `' F " x ) e. dom vol )
37 ismbf 
 |-  ( F : A --> RR -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
38 1 37 syl 
 |-  ( ph -> ( F e. MblFn <-> A. x e. ran (,) ( `' F " x ) e. dom vol ) )
39 36 38 mpbird 
 |-  ( ph -> F e. MblFn )