# 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}={ℤ}_{\ge {M}}$
itgulm.m ${⊢}{\phi }\to {M}\in ℤ$
itgulm.f ${⊢}{\phi }\to {F}:{Z}⟶{𝐿}^{1}$
itgulm.u
itgulm.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
Assertion iblulm ${⊢}{\phi }\to {G}\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 itgulm.z ${⊢}{Z}={ℤ}_{\ge {M}}$
2 itgulm.m ${⊢}{\phi }\to {M}\in ℤ$
3 itgulm.f ${⊢}{\phi }\to {F}:{Z}⟶{𝐿}^{1}$
4 itgulm.u
5 itgulm.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
6 3 ffnd ${⊢}{\phi }\to {F}Fn{Z}$
7 ulmf2
8 6 4 7 syl2anc ${⊢}{\phi }\to {F}:{Z}⟶{ℂ}^{{S}}$
9 eqidd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge {x}\in {S}\right)\right)\to {F}\left({k}\right)\left({x}\right)={F}\left({k}\right)\left({x}\right)$
10 eqidd ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {G}\left({x}\right)={G}\left({x}\right)$
11 1rp ${⊢}1\in {ℝ}^{+}$
12 11 a1i ${⊢}{\phi }\to 1\in {ℝ}^{+}$
13 1 2 8 9 10 4 12 ulmi ${⊢}{\phi }\to \exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1$
14 1 r19.2uz ${⊢}\exists {j}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1$
15 13 14 syl ${⊢}{\phi }\to \exists {k}\in {Z}\phantom{\rule{.4em}{0ex}}\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1$
16 ulmcl
17 4 16 syl ${⊢}{\phi }\to {G}:{S}⟶ℂ$
18 17 adantr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {G}:{S}⟶ℂ$
19 18 feqmptd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {G}=\left({z}\in {S}⟼{G}\left({z}\right)\right)$
20 8 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in \left({ℂ}^{{S}}\right)$
21 elmapi ${⊢}{F}\left({k}\right)\in \left({ℂ}^{{S}}\right)\to {F}\left({k}\right):{S}⟶ℂ$
22 20 21 syl ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right):{S}⟶ℂ$
23 22 adantrr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right):{S}⟶ℂ$
24 23 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\wedge {z}\in {S}\right)\to {F}\left({k}\right)\left({z}\right)\in ℂ$
25 18 ffvelrnda ${⊢}\left(\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\wedge {z}\in {S}\right)\to {G}\left({z}\right)\in ℂ$
26 24 25 nncand ${⊢}\left(\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\wedge {z}\in {S}\right)\to {F}\left({k}\right)\left({z}\right)-\left({F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)={G}\left({z}\right)$
27 26 mpteq2dva ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-\left({F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)=\left({z}\in {S}⟼{G}\left({z}\right)\right)$
28 19 27 eqtr4d ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {G}=\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-\left({F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)$
29 23 feqmptd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right)=\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)\right)$
30 3 ffvelrnda ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)\in {𝐿}^{1}$
31 30 adantrr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right)\in {𝐿}^{1}$
32 29 31 eqeltrrd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)\right)\in {𝐿}^{1}$
33 24 25 subcld ${⊢}\left(\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\wedge {z}\in {S}\right)\to {F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\in ℂ$
34 ulmscl
35 4 34 syl ${⊢}{\phi }\to {S}\in \mathrm{V}$
36 35 adantr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {S}\in \mathrm{V}$
37 36 24 25 29 19 offval2 ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right){-}_{f}{G}=\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)$
38 iblmbf ${⊢}{F}\left({k}\right)\in {𝐿}^{1}\to {F}\left({k}\right)\in MblFn$
39 31 38 syl ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right)\in MblFn$
40 iblmbf ${⊢}{x}\in {𝐿}^{1}\to {x}\in MblFn$
41 40 ssriv ${⊢}{𝐿}^{1}\subseteq MblFn$
42 fss ${⊢}\left({F}:{Z}⟶{𝐿}^{1}\wedge {𝐿}^{1}\subseteq MblFn\right)\to {F}:{Z}⟶MblFn$
43 3 41 42 sylancl ${⊢}{\phi }\to {F}:{Z}⟶MblFn$
44 1 2 43 4 mbfulm ${⊢}{\phi }\to {G}\in MblFn$
45 44 adantr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {G}\in MblFn$
46 39 45 mbfsub ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {F}\left({k}\right){-}_{f}{G}\in MblFn$
47 37 46 eqeltrrd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\in MblFn$
48 eqid ${⊢}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)=\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)$
49 48 33 dmmptd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)={S}$
50 49 fveq2d ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to vol\left(\mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)=vol\left({S}\right)$
51 5 adantr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to vol\left({S}\right)\in ℝ$
52 50 51 eqeltrd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to vol\left(\mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)\in ℝ$
53 1re ${⊢}1\in ℝ$
54 22 ffvelrnda ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {F}\left({k}\right)\left({x}\right)\in ℂ$
55 17 adantr ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {G}:{S}⟶ℂ$
56 55 ffvelrnda ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {G}\left({x}\right)\in ℂ$
57 54 56 subcld ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\in ℂ$
58 57 abscld ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|\in ℝ$
59 ltle ${⊢}\left(\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|\in ℝ\wedge 1\in ℝ\right)\to \left(\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\to \left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|\le 1\right)$
60 58 53 59 sylancl ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left(\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\to \left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|\le 1\right)$
61 fveq2 ${⊢}{z}={x}\to {F}\left({k}\right)\left({z}\right)={F}\left({k}\right)\left({x}\right)$
62 fveq2 ${⊢}{z}={x}\to {G}\left({z}\right)={G}\left({x}\right)$
63 61 62 oveq12d ${⊢}{z}={x}\to {F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)={F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)$
64 ovex ${⊢}{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\in \mathrm{V}$
65 63 48 64 fvmpt ${⊢}{x}\in {S}\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)={F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)$
66 65 adantl ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)={F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)$
67 66 fveq2d ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|=\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|$
68 67 breq1d ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left(\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1↔\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|\le 1\right)$
69 60 68 sylibrd ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left(\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\to \left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1\right)$
70 69 ralimdva ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left(\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1\right)$
71 70 impr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1$
72 49 raleqdv ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left(\forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1↔\forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1\right)$
73 71 72 mpbird ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1$
74 brralrspcev ${⊢}\left(1\in ℝ\wedge \forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le 1\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le {r}$
75 53 73 74 sylancr ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le {r}$
76 bddibl ${⊢}\left(\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\in MblFn\wedge vol\left(\mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)\in ℝ\wedge \exists {r}\in ℝ\phantom{\rule{.4em}{0ex}}\forall {x}\in \mathrm{dom}\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\phantom{\rule{.4em}{0ex}}\left|\left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\left({x}\right)\right|\le {r}\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\in {𝐿}^{1}$
77 47 52 75 76 syl3anc ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\in {𝐿}^{1}$
78 24 32 33 77 iblsub ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to \left({z}\in {S}⟼{F}\left({k}\right)\left({z}\right)-\left({F}\left({k}\right)\left({z}\right)-{G}\left({z}\right)\right)\right)\in {𝐿}^{1}$
79 28 78 eqeltrd ${⊢}\left({\phi }\wedge \left({k}\in {Z}\wedge \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\left|{F}\left({k}\right)\left({x}\right)-{G}\left({x}\right)\right|<1\right)\right)\to {G}\in {𝐿}^{1}$
80 15 79 rexlimddv ${⊢}{\phi }\to {G}\in {𝐿}^{1}$