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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
itgulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
itgulm2.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ 𝐿1 )
itgulm2.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ( ⇝𝑢 ‘ 𝑆 ) ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
itgulm2.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
Assertion itgulm2 ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ∈ 𝐿1 ∧ ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 𝐴 d 𝑥 ) ⇝ ∫ 𝑆 𝐵 d 𝑥 ) )

Proof

Step Hyp Ref Expression
1 itgulm2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 itgulm2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 itgulm2.l ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ 𝐿1 )
4 itgulm2.u ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ( ⇝𝑢 ‘ 𝑆 ) ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
5 itgulm2.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
6 3 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : 𝑍 ⟶ 𝐿1 )
7 1 2 6 4 5 iblulm ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ∈ 𝐿1 )
8 1 2 6 4 5 itgulm ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧 ) ⇝ ∫ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑧 ) d 𝑧 )
9 nfcv ⊢ Ⅎ 𝑘 𝑆
10 nffvmpt1 ⊢ Ⅎ 𝑘 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 )
11 nfcv ⊢ Ⅎ 𝑘 𝑧
12 10 11 nffv ⊢ Ⅎ 𝑘 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 )
13 9 12 nfitg ⊢ Ⅎ 𝑘 ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧
14 nfcv ⊢ Ⅎ 𝑛 ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥
15 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 ) )
16 nfcv ⊢ Ⅎ 𝑥 𝑍
17 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝑆 ↦ 𝐴 )
18 16 17 nfmpt ⊢ Ⅎ 𝑥 ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) )
19 nfcv ⊢ Ⅎ 𝑥 𝑛
20 18 19 nffv ⊢ Ⅎ 𝑥 ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 )
21 nfcv ⊢ Ⅎ 𝑥 𝑧
22 20 21 nffv ⊢ Ⅎ 𝑥 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 )
23 nfcv ⊢ Ⅎ 𝑧 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 )
24 15 22 23 cbvitg ⊢ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧 = ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥
25 fveq2 ⊢ ( 𝑛 = 𝑘 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) = ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) )
26 25 fveq1d ⊢ ( 𝑛 = 𝑘 → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) )
27 26 adantr ⊢ ( ( 𝑛 = 𝑘 ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 ) = ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) )
28 27 itgeq2dv ⊢ ( 𝑛 = 𝑘 → ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 )
29 24 28 syl5eq ⊢ ( 𝑛 = 𝑘 → ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧 = ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 )
30 13 14 29 cbvmpt ⊢ ( 𝑛 ∈ 𝑍 ↦ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧 ) = ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑘 ∈ 𝑍 )
32 ulmscl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ( ⇝𝑢 ‘ 𝑆 ) ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) → 𝑆 ∈ V )
33 mptexg ⊢ ( 𝑆 ∈ V → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V )
34 4 32 33 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V )
35 34 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V )
36 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) )
37 36 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) )
38 31 35 37 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) )
39 38 fveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ‘ 𝑥 ) )
40 simpr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
41 34 ralrimivw ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V )
42 36 fnmpt ⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ V → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) Fn 𝑍 )
43 41 42 syl ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) Fn 𝑍 )
44 ulmf2 ⊢ ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) Fn 𝑍 ∧ ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ( ⇝𝑢 ‘ 𝑆 ) ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ) → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
45 43 4 44 syl2anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
46 45 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( ℂ ↑m 𝑆 ) )
47 elmapi ⊢ ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) : 𝑆 ⟶ ℂ )
49 48 fvmptelrn ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℂ )
50 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐴 )
51 50 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝐴 ∈ ℂ ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
52 40 49 51 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
53 39 52 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) = 𝐴 )
54 53 itgeq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝑆 𝐴 d 𝑥 )
55 54 mpteq2dva ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) = ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 𝐴 d 𝑥 ) )
56 30 55 syl5eq ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ∫ 𝑆 ( ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ‘ 𝑛 ) ‘ 𝑧 ) d 𝑧 ) = ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 𝐴 d 𝑥 ) )
57 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑧 ) = ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 ) )
58 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑧 )
59 nfcv ⊢ Ⅎ 𝑧 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 )
60 57 58 59 cbvitg ⊢ ∫ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑧 ) d 𝑧 = ∫ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥
61 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 )
62 ulmcl ⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) ( ⇝𝑢 ‘ 𝑆 ) ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℂ )
63 4 62 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) : 𝑆 ⟶ ℂ )
64 63 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
65 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 )
66 65 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
67 61 64 66 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
68 67 itgeq2dv ⊢ ( 𝜑 → ∫ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝑆 𝐵 d 𝑥 )
69 60 68 syl5eq ⊢ ( 𝜑 → ∫ 𝑆 ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ‘ 𝑧 ) d 𝑧 = ∫ 𝑆 𝐵 d 𝑥 )
70 8 56 69 3brtr3d ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 𝐴 d 𝑥 ) ⇝ ∫ 𝑆 𝐵 d 𝑥 )
71 7 70 jca ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ∈ 𝐿1 ∧ ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 𝐴 d 𝑥 ) ⇝ ∫ 𝑆 𝐵 d 𝑥 ) )