iblulm

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

	Ref	Expression
Hypotheses	itgulm.z	$⊢ Z = ℤ_{\geq M}$
	itgulm.m	$⊢ φ \to M \in ℤ$
	itgulm.f	$⊢ φ \to F : Z ⟶ 𝐿^{1}$
	itgulm.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
	itgulm.s	$⊢ φ \to vol (S) \in ℝ$
Assertion	iblulm	$⊢ φ \to G \in 𝐿^{1}$

Proof

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

Metamath Proof Explorer

Theorem iblulm

Proof