ulmval

Description: Express the predicate: The sequence of functions F converges uniformly to G on S . (Contributed by Mario Carneiro, 26-Feb-2015)

		Ref	Expression
	Assertion	ulmval	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$

Proof

Step	Hyp	Ref	Expression
1		ulmrel	$⊢ Rel \underset{u}{⇝} (S)$
2	1	brrelex12i	$⊢ F \underset{u}{⇝} (S) G \to (F \in V \land G \in V)$
3	2	a1i	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \to (F \in V \land G \in V))$
4		3simpa	$⊢ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \to (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ)$
5		fvex	$⊢ ℤ_{\geq n} \in V$
6		fex	$⊢ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land ℤ_{\geq n} \in V) \to F \in V$
7	5 6	mpan2	$⊢ F : ℤ_{\geq n} ⟶ ℂ^{S} \to F \in V$
8	7	a1i	$⊢ S \in V \to (F : ℤ_{\geq n} ⟶ ℂ^{S} \to F \in V)$
9		fex	$⊢ (G : S ⟶ ℂ \land S \in V) \to G \in V$
10	9	expcom	$⊢ S \in V \to (G : S ⟶ ℂ \to G \in V)$
11	8 10	anim12d	$⊢ S \in V \to ((F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ) \to (F \in V \land G \in V))$
12	4 11	syl5	$⊢ S \in V \to ((F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \to (F \in V \land G \in V))$
13	12	rexlimdvw	$⊢ S \in V \to (\exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x) \to (F \in V \land G \in V))$
14		df-ulm	$⊢ \underset{u}{⇝} = (s \in V ⟼ \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{s} \land y : s ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x)\})$
15		oveq2	$⊢ s = S \to ℂ^{s} = ℂ^{S}$
16	15	feq3d	$⊢ s = S \to (f : ℤ_{\geq n} ⟶ ℂ^{s} \leftrightarrow f : ℤ_{\geq n} ⟶ ℂ^{S})$
17		feq2	$⊢ s = S \to (y : s ⟶ ℂ \leftrightarrow y : S ⟶ ℂ)$
18		raleq	$⊢ s = S \to (\forall z \in s \|f (k) (z) - y (z)\| < x \leftrightarrow \forall z \in S \|f (k) (z) - y (z)\| < x)$
19	18	rexralbidv	$⊢ s = S \to (\exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x \leftrightarrow \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)$
20	19	ralbidv	$⊢ s = S \to (\forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)$
21	16 17 20	3anbi123d	$⊢ s = S \to ((f : ℤ_{\geq n} ⟶ ℂ^{s} \land y : s ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x) \leftrightarrow (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x))$
22	21	rexbidv	$⊢ s = S \to (\exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{s} \land y : s ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x) \leftrightarrow \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x))$
23	22	opabbidv	$⊢ s = S \to \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{s} \land y : s ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in s \|f (k) (z) - y (z)\| < x)\} = \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\}$
24		elex	$⊢ S \in V \to S \in V$
25		simpr1	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to f : ℤ_{\geq n} ⟶ ℂ^{S}$
26		uzssz	$⊢ ℤ_{\geq n} \subseteq ℤ$
27		ovex	$⊢ ℂ^{S} \in V$
28		zex	$⊢ ℤ \in V$
29		elpm2r	$⊢ ((ℂ^{S} \in V \land ℤ \in V) \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land ℤ_{\geq n} \subseteq ℤ)) \to f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
30	27 28 29	mpanl12	$⊢ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land ℤ_{\geq n} \subseteq ℤ) \to f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
31	25 26 30	sylancl	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ)$
32		simpr2	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to y : S ⟶ ℂ$
33		cnex	$⊢ ℂ \in V$
34		simpl	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to S \in V$
35		elmapg	$⊢ (ℂ \in V \land S \in V) \to (y \in (ℂ^{S}) \leftrightarrow y : S ⟶ ℂ)$
36	33 34 35	sylancr	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to (y \in (ℂ^{S}) \leftrightarrow y : S ⟶ ℂ)$
37	32 36	mpbird	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to y \in (ℂ^{S})$
38	31 37	jca	$⊢ (S \in V \land (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)) \to (f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \land y \in (ℂ^{S}))$
39	38	ex	$⊢ S \in V \to ((f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x) \to (f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \land y \in (ℂ^{S})))$
40	39	rexlimdvw	$⊢ S \in V \to (\exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x) \to (f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \land y \in (ℂ^{S})))$
41	40	ssopab2dv	$⊢ S \in V \to \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} \subseteq \{⟨f, y⟩ \| (f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \land y \in (ℂ^{S}))\}$
42		df-xp	$⊢ ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \times (ℂ^{S}) = \{⟨f, y⟩ \| (f \in ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \land y \in (ℂ^{S}))\}$
43	41 42	sseqtrrdi	$⊢ S \in V \to \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} \subseteq ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \times (ℂ^{S})$
44		ovex	$⊢ (ℂ^{S}) ↑_{𝑝𝑚} ℤ \in V$
45	44 27	xpex	$⊢ ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \times (ℂ^{S}) \in V$
46	45	ssex	$⊢ \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} \subseteq ((ℂ^{S}) ↑_{𝑝𝑚} ℤ) \times (ℂ^{S}) \to \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} \in V$
47	43 46	syl	$⊢ S \in V \to \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} \in V$
48	14 23 24 47	fvmptd3	$⊢ S \in V \to \underset{u}{⇝} (S) = \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\}$
49	48	breqd	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \leftrightarrow F \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} G)$
50		simpl	$⊢ (f = F \land y = G) \to f = F$
51	50	feq1d	$⊢ (f = F \land y = G) \to (f : ℤ_{\geq n} ⟶ ℂ^{S} \leftrightarrow F : ℤ_{\geq n} ⟶ ℂ^{S})$
52		simpr	$⊢ (f = F \land y = G) \to y = G$
53	52	feq1d	$⊢ (f = F \land y = G) \to (y : S ⟶ ℂ \leftrightarrow G : S ⟶ ℂ)$
54	50	fveq1d	$⊢ (f = F \land y = G) \to f (k) = F (k)$
55	54	fveq1d	$⊢ (f = F \land y = G) \to f (k) (z) = F (k) (z)$
56	52	fveq1d	$⊢ (f = F \land y = G) \to y (z) = G (z)$
57	55 56	oveq12d	$⊢ (f = F \land y = G) \to f (k) (z) - y (z) = F (k) (z) - G (z)$
58	57	fveq2d	$⊢ (f = F \land y = G) \to \|f (k) (z) - y (z)\| = \|F (k) (z) - G (z)\|$
59	58	breq1d	$⊢ (f = F \land y = G) \to (\|f (k) (z) - y (z)\| < x \leftrightarrow \|F (k) (z) - G (z)\| < x)$
60	59	ralbidv	$⊢ (f = F \land y = G) \to (\forall z \in S \|f (k) (z) - y (z)\| < x \leftrightarrow \forall z \in S \|F (k) (z) - G (z)\| < x)$
61	60	rexralbidv	$⊢ (f = F \land y = G) \to (\exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x \leftrightarrow \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)$
62	61	ralbidv	$⊢ (f = F \land y = G) \to (\forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)$
63	51 53 62	3anbi123d	$⊢ (f = F \land y = G) \to ((f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x) \leftrightarrow (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
64	63	rexbidv	$⊢ (f = F \land y = G) \to (\exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x) \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
65		eqid	$⊢ \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} = \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\}$
66	64 65	brabga	$⊢ (F \in V \land G \in V) \to (F \{⟨f, y⟩ \| \exists n \in ℤ (f : ℤ_{\geq n} ⟶ ℂ^{S} \land y : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|f (k) (z) - y (z)\| < x)\} G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
67	49 66	sylan9bb	$⊢ (S \in V \land (F \in V \land G \in V)) \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$
68	67	ex	$⊢ S \in V \to ((F \in V \land G \in V) \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x)))$
69	3 13 68	pm5.21ndd	$⊢ S \in V \to (F \underset{u}{⇝} (S) G \leftrightarrow \exists n \in ℤ (F : ℤ_{\geq n} ⟶ ℂ^{S} \land G : S ⟶ ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < x))$

Metamath Proof Explorer

Theorem ulmval

Proof