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 = ℤ_{\geq M}$
	itgulm2.m	$⊢ φ \to M \in ℤ$
	itgulm2.l	$⊢ (φ \land k \in Z) \to (x \in S ⟼ A) \in 𝐿^{1}$
	itgulm2.u	$⊢ φ \to (k \in Z ⟼ (x \in S ⟼ A)) \underset{u}{⇝} (S) (x \in S ⟼ B)$
	itgulm2.s	$⊢ φ \to vol (S) \in ℝ$
Assertion	itgulm2	$⊢ φ \to ((x \in S ⟼ B) \in 𝐿^{1} \land (k \in Z ⟼ \int_{S} A d x) ⇝ \int_{S} B d x)$

Proof

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

Metamath Proof Explorer

Theorem itgulm2

Proof