Metamath Proof Explorer

Theorem mbfss

Description: Change the domain of a measurability predicate. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses mbfss.1 
|- ( ph -> A C_ B )
mbfss.2 
|- ( ph -> B e. dom vol )
mbfss.3 
|- ( ( ph /\ x e. A ) -> C e. V )
mbfss.4 
|- ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )
mbfss.5 
|- ( ph -> ( x e. A |-> C ) e. MblFn )
Assertion mbfss 
|- ( ph -> ( x e. B |-> C ) e. MblFn )

Proof

Step Hyp Ref Expression
1 mbfss.1 
 |-  ( ph -> A C_ B )
2 mbfss.2 
 |-  ( ph -> B e. dom vol )
3 mbfss.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 mbfss.4 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )
5 mbfss.5 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
6 elun 
 |-  ( x e. ( A u. ( B \ A ) ) <-> ( x e. A \/ x e. ( B \ A ) ) )
7 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
8 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
9 1 8 sylib 
 |-  ( ph -> ( A u. B ) = B )
10 7 9 syl5eq 
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
11 10 eleq2d 
 |-  ( ph -> ( x e. ( A u. ( B \ A ) ) <-> x e. B ) )
12 6 11 bitr3id 
 |-  ( ph -> ( ( x e. A \/ x e. ( B \ A ) ) <-> x e. B ) )
13 12 biimpar 
 |-  ( ( ph /\ x e. B ) -> ( x e. A \/ x e. ( B \ A ) ) )
14 5 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
15 0cn 
 |-  0 e. CC
16 4 15 eqeltrdi 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C e. CC )
17 14 16 jaodan 
 |-  ( ( ph /\ ( x e. A \/ x e. ( B \ A ) ) ) -> C e. CC )
18 13 17 syldan 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
19 18 recld 
 |-  ( ( ph /\ x e. B ) -> ( Re ` C ) e. RR )
20 19 fmpttd 
 |-  ( ph -> ( x e. B |-> ( Re ` C ) ) : B --> RR )
21 1 resmptd 
 |-  ( ph -> ( ( x e. B |-> ( Re ` C ) ) |` A ) = ( x e. A |-> ( Re ` C ) ) )
22 14 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn <-> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) ) )
23 5 22 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` C ) ) e. MblFn /\ ( x e. A |-> ( Im ` C ) ) e. MblFn ) )
24 23 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` C ) ) e. MblFn )
25 21 24 eqeltrd 
 |-  ( ph -> ( ( x e. B |-> ( Re ` C ) ) |` A ) e. MblFn )
26 difss 
 |-  ( B \ A ) C_ B
27 resmpt 
 |-  ( ( B \ A ) C_ B -> ( ( x e. B |-> ( Re ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> ( Re ` C ) ) )
28 26 27 ax-mp 
 |-  ( ( x e. B |-> ( Re ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> ( Re ` C ) )
29 4 fveq2d 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Re ` C ) = ( Re ` 0 ) )
30 re0 
 |-  ( Re ` 0 ) = 0
31 29 30 eqtrdi 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Re ` C ) = 0 )
32 31 mpteq2dva 
 |-  ( ph -> ( x e. ( B \ A ) |-> ( Re ` C ) ) = ( x e. ( B \ A ) |-> 0 ) )
33 28 32 syl5eq 
 |-  ( ph -> ( ( x e. B |-> ( Re ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> 0 ) )
34 fconstmpt 
 |-  ( ( B \ A ) X. { 0 } ) = ( x e. ( B \ A ) |-> 0 )
35 5 3 mbfdm2 
 |-  ( ph -> A e. dom vol )
36 difmbl 
 |-  ( ( B e. dom vol /\ A e. dom vol ) -> ( B \ A ) e. dom vol )
37 2 35 36 syl2anc 
 |-  ( ph -> ( B \ A ) e. dom vol )
38 mbfconst 
 |-  ( ( ( B \ A ) e. dom vol /\ 0 e. CC ) -> ( ( B \ A ) X. { 0 } ) e. MblFn )
39 37 15 38 sylancl 
 |-  ( ph -> ( ( B \ A ) X. { 0 } ) e. MblFn )
40 34 39 eqeltrrid 
 |-  ( ph -> ( x e. ( B \ A ) |-> 0 ) e. MblFn )
41 33 40 eqeltrd 
 |-  ( ph -> ( ( x e. B |-> ( Re ` C ) ) |` ( B \ A ) ) e. MblFn )
42 20 25 41 10 mbfres2 
 |-  ( ph -> ( x e. B |-> ( Re ` C ) ) e. MblFn )
43 18 imcld 
 |-  ( ( ph /\ x e. B ) -> ( Im ` C ) e. RR )
44 43 fmpttd 
 |-  ( ph -> ( x e. B |-> ( Im ` C ) ) : B --> RR )
45 1 resmptd 
 |-  ( ph -> ( ( x e. B |-> ( Im ` C ) ) |` A ) = ( x e. A |-> ( Im ` C ) ) )
46 23 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` C ) ) e. MblFn )
47 45 46 eqeltrd 
 |-  ( ph -> ( ( x e. B |-> ( Im ` C ) ) |` A ) e. MblFn )
48 resmpt 
 |-  ( ( B \ A ) C_ B -> ( ( x e. B |-> ( Im ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> ( Im ` C ) ) )
49 26 48 ax-mp 
 |-  ( ( x e. B |-> ( Im ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> ( Im ` C ) )
50 4 fveq2d 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Im ` C ) = ( Im ` 0 ) )
51 im0 
 |-  ( Im ` 0 ) = 0
52 50 51 eqtrdi 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> ( Im ` C ) = 0 )
53 52 mpteq2dva 
 |-  ( ph -> ( x e. ( B \ A ) |-> ( Im ` C ) ) = ( x e. ( B \ A ) |-> 0 ) )
54 49 53 syl5eq 
 |-  ( ph -> ( ( x e. B |-> ( Im ` C ) ) |` ( B \ A ) ) = ( x e. ( B \ A ) |-> 0 ) )
55 54 40 eqeltrd 
 |-  ( ph -> ( ( x e. B |-> ( Im ` C ) ) |` ( B \ A ) ) e. MblFn )
56 44 47 55 10 mbfres2 
 |-  ( ph -> ( x e. B |-> ( Im ` C ) ) e. MblFn )
57 18 ismbfcn2 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn <-> ( ( x e. B |-> ( Re ` C ) ) e. MblFn /\ ( x e. B |-> ( Im ` C ) ) e. MblFn ) ) )
58 42 56 57 mpbir2and 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )