Metamath Proof Explorer

Theorem iblulm

Description: A uniform limit of integrable functions is integrable. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses itgulm.z 
|- Z = ( ZZ>= ` M )
itgulm.m 
|- ( ph -> M e. ZZ )
itgulm.f 
|- ( ph -> F : Z --> L^1 )
itgulm.u 
|- ( ph -> F ( ~~>u ` S ) G )
itgulm.s 
|- ( ph -> ( vol ` S ) e. RR )
Assertion iblulm 
|- ( ph -> G e. L^1 )

Proof

Step Hyp Ref Expression
1 itgulm.z 
 |-  Z = ( ZZ>= ` M )
2 itgulm.m 
 |-  ( ph -> M e. ZZ )
3 itgulm.f 
 |-  ( ph -> F : Z --> L^1 )
4 itgulm.u 
 |-  ( ph -> F ( ~~>u ` S ) G )
5 itgulm.s 
 |-  ( ph -> ( vol ` S ) e. RR )
6 3 ffnd 
 |-  ( ph -> F Fn Z )
7 ulmf2 
 |-  ( ( F Fn Z /\ F ( ~~>u ` S ) G ) -> F : Z --> ( CC ^m S ) )
8 6 4 7 syl2anc 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
9 eqidd 
 |-  ( ( ph /\ ( k e. Z /\ x e. S ) ) -> ( ( F ` k ) ` x ) = ( ( F ` k ) ` x ) )
10 eqidd 
 |-  ( ( ph /\ x e. S ) -> ( G ` x ) = ( G ` x ) )
11 1rp 
 |-  1 e. RR+
12 11 a1i 
 |-  ( ph -> 1 e. RR+ )
13 1 2 8 9 10 4 12 ulmi 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 )
14 1 r19.2uz 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 -> E. k e. Z A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 )
15 13 14 syl 
 |-  ( ph -> E. k e. Z A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 )
16 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
17 4 16 syl 
 |-  ( ph -> G : S --> CC )
18 17 adantr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> G : S --> CC )
19 18 feqmptd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> G = ( z e. S |-> ( G ` z ) ) )
20 8 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
21 elmapi 
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
22 20 21 syl 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) : S --> CC )
23 22 adantrr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( F ` k ) : S --> CC )
24 23 ffvelcdmda 
 |-  ( ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) /\ z e. S ) -> ( ( F ` k ) ` z ) e. CC )
25 18 ffvelcdmda 
 |-  ( ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) /\ z e. S ) -> ( G ` z ) e. CC )
26 24 25 nncand 
 |-  ( ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) /\ z e. S ) -> ( ( ( F ` k ) ` z ) - ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = ( G ` z ) )
27 26 mpteq2dva 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( z e. S |-> ( ( ( F ` k ) ` z ) - ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) = ( z e. S |-> ( G ` z ) ) )
28 19 27 eqtr4d 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> G = ( z e. S |-> ( ( ( F ` k ) ` z ) - ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) )
29 23 feqmptd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( F ` k ) = ( z e. S |-> ( ( F ` k ) ` z ) ) )
30 3 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. L^1 )
31 30 adantrr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( F ` k ) e. L^1 )
32 29 31 eqeltrrd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( z e. S |-> ( ( F ` k ) ` z ) ) e. L^1 )
33 24 25 subcld 
 |-  ( ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) /\ z e. S ) -> ( ( ( F ` k ) ` z ) - ( G ` z ) ) e. CC )
34 ulmscl 
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
35 4 34 syl 
 |-  ( ph -> S e. _V )
36 35 adantr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> S e. _V )
37 36 24 25 29 19 offval2 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( ( F ` k ) oF - G ) = ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) )
38 iblmbf 
 |-  ( ( F ` k ) e. L^1 -> ( F ` k ) e. MblFn )
39 31 38 syl 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( F ` k ) e. MblFn )
40 iblmbf 
 |-  ( x e. L^1 -> x e. MblFn )
41 40 ssriv 
 |-  L^1 C_ MblFn
42 fss 
 |-  ( ( F : Z --> L^1 /\ L^1 C_ MblFn ) -> F : Z --> MblFn )
43 3 41 42 sylancl 
 |-  ( ph -> F : Z --> MblFn )
44 1 2 43 4 mbfulm 
 |-  ( ph -> G e. MblFn )
45 44 adantr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> G e. MblFn )
46 39 45 mbfsub 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( ( F ` k ) oF - G ) e. MblFn )
47 37 46 eqeltrrd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) e. MblFn )
48 eqid 
 |-  ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) )
49 48 33 dmmptd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = S )
50 49 fveq2d 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( vol ` dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) = ( vol ` S ) )
51 5 adantr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( vol ` S ) e. RR )
52 50 51 eqeltrd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( vol ` dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) e. RR )
53 1re 
 |-  1 e. RR
54 22 ffvelcdmda 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( F ` k ) ` x ) e. CC )
55 17 adantr 
 |-  ( ( ph /\ k e. Z ) -> G : S --> CC )
56 55 ffvelcdmda 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( G ` x ) e. CC )
57 54 56 subcld 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( ( F ` k ) ` x ) - ( G ` x ) ) e. CC )
58 57 abscld 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) e. RR )
59 ltle 
 |-  ( ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) <_ 1 ) )
60 58 53 59 sylancl 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 -> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) <_ 1 ) )
61 fveq2 
 |-  ( z = x -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` x ) )
62 fveq2 
 |-  ( z = x -> ( G ` z ) = ( G ` x ) )
63 61 62 oveq12d 
 |-  ( z = x -> ( ( ( F ` k ) ` z ) - ( G ` z ) ) = ( ( ( F ` k ) ` x ) - ( G ` x ) ) )
64 ovex 
 |-  ( ( ( F ` k ) ` x ) - ( G ` x ) ) e. _V
65 63 48 64 fvmpt 
 |-  ( x e. S -> ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) = ( ( ( F ` k ) ` x ) - ( G ` x ) ) )
66 65 adantl 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) = ( ( ( F ` k ) ` x ) - ( G ` x ) ) )
67 66 fveq2d 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) = ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) )
68 67 breq1d 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 <-> ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) <_ 1 ) )
69 60 68 sylibrd 
 |-  ( ( ( ph /\ k e. Z ) /\ x e. S ) -> ( ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 -> ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 ) )
70 69 ralimdva 
 |-  ( ( ph /\ k e. Z ) -> ( A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 -> A. x e. S ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 ) )
71 70 impr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> A. x e. S ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 )
72 71 49 raleqtrrdv 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> A. x e. dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 )
73 brralrspcev 
 |-  ( ( 1 e. RR /\ A. x e. dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ 1 ) -> E. r e. RR A. x e. dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ r )
74 53 72 73 sylancr 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> E. r e. RR A. x e. dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ r )
75 bddibl 
 |-  ( ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) e. MblFn /\ ( vol ` dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) e. RR /\ E. r e. RR A. x e. dom ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ( abs ` ( ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ` x ) ) <_ r ) -> ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) e. L^1 )
76 47 52 74 75 syl3anc 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( z e. S |-> ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) e. L^1 )
77 24 32 33 76 iblsub 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> ( z e. S |-> ( ( ( F ` k ) ` z ) - ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) ) e. L^1 )
78 28 77 eqeltrd 
 |-  ( ( ph /\ ( k e. Z /\ A. x e. S ( abs ` ( ( ( F ` k ) ` x ) - ( G ` x ) ) ) < 1 ) ) -> G e. L^1 )
79 15 78 rexlimddv 
 |-  ( ph -> G e. L^1 )