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 )