Metamath Proof Explorer

Theorem iblss2

Description: Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 iblss2.1 
 |-  ( ph -> A C_ B )
2 iblss2.2 
 |-  ( ph -> B e. dom vol )
3 iblss2.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 iblss2.4 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C = 0 )
5 iblss2.5 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
6 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
7 5 6 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
8 1 2 3 4 7 mbfss 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )
9 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A C_ B )
10 9 sselda 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> x e. B )
11 10 iftrued 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
12 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
13 12 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
14 11 13 eqtr4d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
15 ifid 
 |-  if ( x e. B , 0 , 0 ) = 0
16 simplll 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ph )
17 simpr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> x e. B )
18 simplr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> -. x e. A )
19 17 18 eldifd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> x e. ( B \ A ) )
20 16 19 4 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> C = 0 )
21 20 oveq1d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ( C / ( _i ^ k ) ) = ( 0 / ( _i ^ k ) ) )
22 simpllr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> k e. ( 0 ... 3 ) )
23 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
24 ax-icn 
 |-  _i e. CC
25 ine0 
 |-  _i =/= 0
26 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
27 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
28 26 27 div0d 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( 0 / ( _i ^ k ) ) = 0 )
29 24 25 28 mp3an12 
 |-  ( k e. ZZ -> ( 0 / ( _i ^ k ) ) = 0 )
30 22 23 29 3syl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ( 0 / ( _i ^ k ) ) = 0 )
31 21 30 eqtrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ( C / ( _i ^ k ) ) = 0 )
32 31 fveq2d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` 0 ) )
33 re0 
 |-  ( Re ` 0 ) = 0
34 32 33 eqtrdi 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = 0 )
35 34 ifeq1d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , 0 , 0 ) )
36 ifid 
 |-  if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , 0 , 0 ) = 0
37 35 36 eqtrdi 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = 0 )
38 37 ifeq1da 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. B , 0 , 0 ) )
39 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
40 39 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
41 15 38 40 3eqtr4a 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
42 14 41 pm2.61dan 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
43 ifan 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
44 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
45 42 43 44 3eqtr4g 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
46 45 mpteq2dv 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
47 46 fveq2d 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
48 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
49 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
50 48 49 5 3 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
51 23 50 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
52 47 51 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
53 52 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
54 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
55 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
56 elun 
 |-  ( x e. ( A u. ( B \ A ) ) <-> ( x e. A \/ x e. ( B \ A ) ) )
57 undif2 
 |-  ( A u. ( B \ A ) ) = ( A u. B )
58 ssequn1 
 |-  ( A C_ B <-> ( A u. B ) = B )
59 1 58 sylib 
 |-  ( ph -> ( A u. B ) = B )
60 57 59 syl5eq 
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
61 60 eleq2d 
 |-  ( ph -> ( x e. ( A u. ( B \ A ) ) <-> x e. B ) )
62 56 61 bitr3id 
 |-  ( ph -> ( ( x e. A \/ x e. ( B \ A ) ) <-> x e. B ) )
63 62 biimpar 
 |-  ( ( ph /\ x e. B ) -> ( x e. A \/ x e. ( B \ A ) ) )
64 7 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
65 0cn 
 |-  0 e. CC
66 4 65 eqeltrdi 
 |-  ( ( ph /\ x e. ( B \ A ) ) -> C e. CC )
67 64 66 jaodan 
 |-  ( ( ph /\ ( x e. A \/ x e. ( B \ A ) ) ) -> C e. CC )
68 63 67 syldan 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
69 54 55 68 isibl2 
 |-  ( ph -> ( ( x e. B |-> C ) e. L^1 <-> ( ( x e. B |-> C ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
70 8 53 69 mpbir2and 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )