# Metamath Proof Explorer

## Theorem itgulm2

Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses itgulm2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
itgulm2.m ${⊢}{\phi }\to {M}\in ℤ$
itgulm2.l ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({x}\in {S}⟼{A}\right)\in {𝐿}^{1}$
itgulm2.u
itgulm2.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
Assertion itgulm2 ${⊢}{\phi }\to \left(\left({x}\in {S}⟼{B}\right)\in {𝐿}^{1}\wedge \left({k}\in {Z}⟼{\int }_{{S}}{A}d{x}\right)⇝{\int }_{{S}}{B}d{x}\right)$

### Proof

Step Hyp Ref Expression
1 itgulm2.z ${⊢}{Z}={ℤ}_{\ge {M}}$
2 itgulm2.m ${⊢}{\phi }\to {M}\in ℤ$
3 itgulm2.l ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({x}\in {S}⟼{A}\right)\in {𝐿}^{1}$
4 itgulm2.u
5 itgulm2.s ${⊢}{\phi }\to vol\left({S}\right)\in ℝ$
6 3 fmpttd ${⊢}{\phi }\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right):{Z}⟶{𝐿}^{1}$
7 1 2 6 4 5 iblulm ${⊢}{\phi }\to \left({x}\in {S}⟼{B}\right)\in {𝐿}^{1}$
8 1 2 6 4 5 itgulm ${⊢}{\phi }\to \left({n}\in {Z}⟼{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}\right)⇝{\int }_{{S}}\left({x}\in {S}⟼{B}\right)\left({z}\right)d{z}$
9 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{S}$
10 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)$
11 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{z}$
12 10 11 nffv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)$
13 9 12 nfitg ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}$
14 nfcv ${⊢}\underset{_}{Ⅎ}{n}\phantom{\rule{.4em}{0ex}}{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}$
15 fveq2 ${⊢}{z}={x}\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)=\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)$
16 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{Z}$
17 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}⟼{A}\right)$
18 16 17 nfmpt ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)$
19 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{n}$
20 18 19 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)$
21 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
22 20 21 nffv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)$
23 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)$
24 15 22 23 cbvitg ${⊢}{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}={\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)d{x}$
25 fveq2 ${⊢}{n}={k}\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)=\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)$
26 25 fveq1d ${⊢}{n}={k}\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)=\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)$
27 26 adantr ${⊢}\left({n}={k}\wedge {x}\in {S}\right)\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)=\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)$
28 27 itgeq2dv ${⊢}{n}={k}\to {\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({x}\right)d{x}={\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}$
29 24 28 syl5eq ${⊢}{n}={k}\to {\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}={\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}$
30 13 14 29 cbvmpt ${⊢}\left({n}\in {Z}⟼{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}\right)=\left({k}\in {Z}⟼{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}\right)$
31 simplr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {k}\in {Z}$
32 ulmscl
33 mptexg ${⊢}{S}\in \mathrm{V}\to \left({x}\in {S}⟼{A}\right)\in \mathrm{V}$
34 4 32 33 3syl ${⊢}{\phi }\to \left({x}\in {S}⟼{A}\right)\in \mathrm{V}$
35 34 ad2antrr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({x}\in {S}⟼{A}\right)\in \mathrm{V}$
36 eqid ${⊢}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)=\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)$
37 36 fvmpt2 ${⊢}\left({k}\in {Z}\wedge \left({x}\in {S}⟼{A}\right)\in \mathrm{V}\right)\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)=\left({x}\in {S}⟼{A}\right)$
38 31 35 37 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)=\left({x}\in {S}⟼{A}\right)$
39 38 fveq1d ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)=\left({x}\in {S}⟼{A}\right)\left({x}\right)$
40 simpr ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {x}\in {S}$
41 34 ralrimivw ${⊢}{\phi }\to \forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}⟼{A}\right)\in \mathrm{V}$
42 36 fnmpt ${⊢}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}⟼{A}\right)\in \mathrm{V}\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)Fn{Z}$
43 41 42 syl ${⊢}{\phi }\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)Fn{Z}$
44 ulmf2
45 43 4 44 syl2anc ${⊢}{\phi }\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right):{Z}⟶{ℂ}^{{S}}$
46 45 fvmptelrn ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({x}\in {S}⟼{A}\right)\in \left({ℂ}^{{S}}\right)$
47 elmapi ${⊢}\left({x}\in {S}⟼{A}\right)\in \left({ℂ}^{{S}}\right)\to \left({x}\in {S}⟼{A}\right):{S}⟶ℂ$
48 46 47 syl ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to \left({x}\in {S}⟼{A}\right):{S}⟶ℂ$
49 48 fvmptelrn ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to {A}\in ℂ$
50 eqid ${⊢}\left({x}\in {S}⟼{A}\right)=\left({x}\in {S}⟼{A}\right)$
51 50 fvmpt2 ${⊢}\left({x}\in {S}\wedge {A}\in ℂ\right)\to \left({x}\in {S}⟼{A}\right)\left({x}\right)={A}$
52 40 49 51 syl2anc ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({x}\in {S}⟼{A}\right)\left({x}\right)={A}$
53 39 52 eqtrd ${⊢}\left(\left({\phi }\wedge {k}\in {Z}\right)\wedge {x}\in {S}\right)\to \left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)={A}$
54 53 itgeq2dv ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}={\int }_{{S}}{A}d{x}$
55 54 mpteq2dva ${⊢}{\phi }\to \left({k}\in {Z}⟼{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({k}\right)\left({x}\right)d{x}\right)=\left({k}\in {Z}⟼{\int }_{{S}}{A}d{x}\right)$
56 30 55 syl5eq ${⊢}{\phi }\to \left({n}\in {Z}⟼{\int }_{{S}}\left({k}\in {Z}⟼\left({x}\in {S}⟼{A}\right)\right)\left({n}\right)\left({z}\right)d{z}\right)=\left({k}\in {Z}⟼{\int }_{{S}}{A}d{x}\right)$
57 fveq2 ${⊢}{z}={x}\to \left({x}\in {S}⟼{B}\right)\left({z}\right)=\left({x}\in {S}⟼{B}\right)\left({x}\right)$
58 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}⟼{B}\right)\left({z}\right)$
59 nfcv ${⊢}\underset{_}{Ⅎ}{z}\phantom{\rule{.4em}{0ex}}\left({x}\in {S}⟼{B}\right)\left({x}\right)$
60 57 58 59 cbvitg ${⊢}{\int }_{{S}}\left({x}\in {S}⟼{B}\right)\left({z}\right)d{z}={\int }_{{S}}\left({x}\in {S}⟼{B}\right)\left({x}\right)d{x}$
61 simpr ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {x}\in {S}$
62 ulmcl
63 4 62 syl ${⊢}{\phi }\to \left({x}\in {S}⟼{B}\right):{S}⟶ℂ$
64 63 fvmptelrn ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to {B}\in ℂ$
65 eqid ${⊢}\left({x}\in {S}⟼{B}\right)=\left({x}\in {S}⟼{B}\right)$
66 65 fvmpt2 ${⊢}\left({x}\in {S}\wedge {B}\in ℂ\right)\to \left({x}\in {S}⟼{B}\right)\left({x}\right)={B}$
67 61 64 66 syl2anc ${⊢}\left({\phi }\wedge {x}\in {S}\right)\to \left({x}\in {S}⟼{B}\right)\left({x}\right)={B}$
68 67 itgeq2dv ${⊢}{\phi }\to {\int }_{{S}}\left({x}\in {S}⟼{B}\right)\left({x}\right)d{x}={\int }_{{S}}{B}d{x}$
69 60 68 syl5eq ${⊢}{\phi }\to {\int }_{{S}}\left({x}\in {S}⟼{B}\right)\left({z}\right)d{z}={\int }_{{S}}{B}d{x}$
70 8 56 69 3brtr3d ${⊢}{\phi }\to \left({k}\in {Z}⟼{\int }_{{S}}{A}d{x}\right)⇝{\int }_{{S}}{B}d{x}$
71 7 70 jca ${⊢}{\phi }\to \left(\left({x}\in {S}⟼{B}\right)\in {𝐿}^{1}\wedge \left({k}\in {Z}⟼{\int }_{{S}}{A}d{x}\right)⇝{\int }_{{S}}{B}d{x}\right)$