ulmbdd

Description: A uniform limit of bounded functions is bounded. (Contributed by Mario Carneiro, 27-Feb-2015)

	Ref	Expression
Hypotheses	ulmbdd.z	$⊢ Z = ℤ_{\geq M}$
	ulmbdd.m	$⊢ φ \to M \in ℤ$
	ulmbdd.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	ulmbdd.b	$⊢ (φ \land k \in Z) \to \exists x \in ℝ \forall z \in S \|F (k) (z)\| \leq x$
	ulmbdd.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
Assertion	ulmbdd	$⊢ φ \to \exists x \in ℝ \forall z \in S \|G (z)\| \leq x$

Proof

Step	Hyp	Ref	Expression
1		ulmbdd.z	$⊢ Z = ℤ_{\geq M}$
2		ulmbdd.m	$⊢ φ \to M \in ℤ$
3		ulmbdd.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
4		ulmbdd.b	$⊢ (φ \land k \in Z) \to \exists x \in ℝ \forall z \in S \|F (k) (z)\| \leq x$
5		ulmbdd.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
6		eqidd	$⊢ (φ \land (k \in Z \land z \in S)) \to F (k) (z) = F (k) (z)$
7		eqidd	$⊢ (φ \land z \in S) \to G (z) = G (z)$
8		1rp	$⊢ 1 \in ℝ^{+}$
9	8	a1i	$⊢ φ \to 1 \in ℝ^{+}$
10	1 2 3 6 7 5 9	ulmi	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < 1$
11	1	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists k \in Z \forall z \in S \|F (k) (z) - G (z)\| < 1$
12		r19.26	$⊢ \forall z \in S (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1) \leftrightarrow (\forall z \in S \|F (k) (z)\| \leq x \land \forall z \in S \|F (k) (z) - G (z)\| < 1)$
13		peano2re	$⊢ x \in ℝ \to x + 1 \in ℝ$
14	13	adantl	$⊢ ((φ \land k \in Z) \land x \in ℝ) \to x + 1 \in ℝ$
15		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
16	5 15	syl	$⊢ φ \to G : S ⟶ ℂ$
17	16	ad3antrrr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to G : S ⟶ ℂ$
18		simprl	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to z \in S$
19	17 18	ffvelcdmd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to G (z) \in ℂ$
20	19	abscld	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z)\| \in ℝ$
21	3	ad3antrrr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to F : Z ⟶ ℂ^{S}$
22		simpllr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to k \in Z$
23	21 22	ffvelcdmd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to F (k) \in (ℂ^{S})$
24		elmapi	$⊢ F (k) \in (ℂ^{S}) \to F (k) : S ⟶ ℂ$
25	23 24	syl	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to F (k) : S ⟶ ℂ$
26	25 18	ffvelcdmd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to F (k) (z) \in ℂ$
27	26	abscld	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z)\| \in ℝ$
28	19 26	subcld	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to G (z) - F (k) (z) \in ℂ$
29	28	abscld	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z) - F (k) (z)\| \in ℝ$
30	27 29	readdcld	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z)\| + \|G (z) - F (k) (z)\| \in ℝ$
31	14	adantr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to x + 1 \in ℝ$
32	26 19	pncan3d	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to F (k) (z) + G (z) - F (k) (z) = G (z)$
33	32	fveq2d	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z) + G (z) - F (k) (z)\| = \|G (z)\|$
34	26 28	abstrid	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z) + G (z) - F (k) (z)\| \leq \|F (k) (z)\| + \|G (z) - F (k) (z)\|$
35	33 34	eqbrtrrd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z)\| \leq \|F (k) (z)\| + \|G (z) - F (k) (z)\|$
36		simplr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to x \in ℝ$
37		1re	$⊢ 1 \in ℝ$
38	37	a1i	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to 1 \in ℝ$
39		simprrl	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z)\| \leq x$
40	19 26	abssubd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z) - F (k) (z)\| = \|F (k) (z) - G (z)\|$
41		simprrr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z) - G (z)\| < 1$
42	40 41	eqbrtrd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z) - F (k) (z)\| < 1$
43		ltle	$⊢ (\|G (z) - F (k) (z)\| \in ℝ \land 1 \in ℝ) \to (\|G (z) - F (k) (z)\| < 1 \to \|G (z) - F (k) (z)\| \leq 1)$
44	29 37 43	sylancl	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to (\|G (z) - F (k) (z)\| < 1 \to \|G (z) - F (k) (z)\| \leq 1)$
45	42 44	mpd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z) - F (k) (z)\| \leq 1$
46	27 29 36 38 39 45	le2addd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|F (k) (z)\| + \|G (z) - F (k) (z)\| \leq x + 1$
47	20 30 31 35 46	letrd	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land (z \in S \land (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1))) \to \|G (z)\| \leq x + 1$
48	47	expr	$⊢ (((φ \land k \in Z) \land x \in ℝ) \land z \in S) \to ((\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1) \to \|G (z)\| \leq x + 1)$
49	48	ralimdva	$⊢ ((φ \land k \in Z) \land x \in ℝ) \to (\forall z \in S (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1) \to \forall z \in S \|G (z)\| \leq x + 1)$
50		brralrspcev	$⊢ (x + 1 \in ℝ \land \forall z \in S \|G (z)\| \leq x + 1) \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y$
51	14 49 50	syl6an	$⊢ ((φ \land k \in Z) \land x \in ℝ) \to (\forall z \in S (\|F (k) (z)\| \leq x \land \|F (k) (z) - G (z)\| < 1) \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y)$
52	12 51	biimtrrid	$⊢ ((φ \land k \in Z) \land x \in ℝ) \to ((\forall z \in S \|F (k) (z)\| \leq x \land \forall z \in S \|F (k) (z) - G (z)\| < 1) \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y)$
53	52	expd	$⊢ ((φ \land k \in Z) \land x \in ℝ) \to (\forall z \in S \|F (k) (z)\| \leq x \to (\forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y))$
54	53	rexlimdva	$⊢ (φ \land k \in Z) \to (\exists x \in ℝ \forall z \in S \|F (k) (z)\| \leq x \to (\forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y))$
55	4 54	mpd	$⊢ (φ \land k \in Z) \to (\forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists y \in ℝ \forall z \in S \|G (z)\| \leq y)$
56		breq2	$⊢ y = x \to (\|G (z)\| \leq y \leftrightarrow \|G (z)\| \leq x)$
57	56	ralbidv	$⊢ y = x \to (\forall z \in S \|G (z)\| \leq y \leftrightarrow \forall z \in S \|G (z)\| \leq x)$
58	57	cbvrexvw	$⊢ \exists y \in ℝ \forall z \in S \|G (z)\| \leq y \leftrightarrow \exists x \in ℝ \forall z \in S \|G (z)\| \leq x$
59	55 58	imbitrdi	$⊢ (φ \land k \in Z) \to (\forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists x \in ℝ \forall z \in S \|G (z)\| \leq x)$
60	59	rexlimdva	$⊢ φ \to (\exists k \in Z \forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists x \in ℝ \forall z \in S \|G (z)\| \leq x)$
61	11 60	syl5	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < 1 \to \exists x \in ℝ \forall z \in S \|G (z)\| \leq x)$
62	10 61	mpd	$⊢ φ \to \exists x \in ℝ \forall z \in S \|G (z)\| \leq x$

Metamath Proof Explorer

Theorem ulmbdd

Proof