ulmss

Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015)

	Ref	Expression
Hypotheses	ulmss.z	$⊢ Z = ℤ_{\geq M}$
	ulmss.t	$⊢ φ \to T \subseteq S$
	ulmss.a	$⊢ (φ \land x \in Z) \to A \in W$
	ulmss.u	$⊢ φ \to (x \in Z ⟼ A) \underset{u}{⇝} (S) G$
Assertion	ulmss	$⊢ φ \to (x \in Z ⟼ {A ↾}_{T}) \underset{u}{⇝} (T) ({G ↾}_{T})$

Proof

Step	Hyp	Ref	Expression
1		ulmss.z	$⊢ Z = ℤ_{\geq M}$
2		ulmss.t	$⊢ φ \to T \subseteq S$
3		ulmss.a	$⊢ (φ \land x \in Z) \to A \in W$
4		ulmss.u	$⊢ φ \to (x \in Z ⟼ A) \underset{u}{⇝} (S) G$
5	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
6	2	adantr	$⊢ (φ \land k \in Z) \to T \subseteq S$
7		ssralv	$⊢ T \subseteq S \to (\forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall z \in T \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
8	6 7	syl	$⊢ (φ \land k \in Z) \to (\forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall z \in T \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
9		fvres	$⊢ z \in T \to ({A ↾}_{T}) (z) = A (z)$
10	9	ad2antll	$⊢ (φ \land (x \in Z \land z \in T)) \to ({A ↾}_{T}) (z) = A (z)$
11		simprl	$⊢ (φ \land (x \in Z \land z \in T)) \to x \in Z$
12	3	adantrr	$⊢ (φ \land (x \in Z \land z \in T)) \to A \in W$
13		resexg	$⊢ A \in W \to {A ↾}_{T} \in V$
14	12 13	syl	$⊢ (φ \land (x \in Z \land z \in T)) \to {A ↾}_{T} \in V$
15		eqid	$⊢ (x \in Z ⟼ {A ↾}_{T}) = (x \in Z ⟼ {A ↾}_{T})$
16	15	fvmpt2	$⊢ (x \in Z \land {A ↾}_{T} \in V) \to (x \in Z ⟼ {A ↾}_{T}) (x) = {A ↾}_{T}$
17	11 14 16	syl2anc	$⊢ (φ \land (x \in Z \land z \in T)) \to (x \in Z ⟼ {A ↾}_{T}) (x) = {A ↾}_{T}$
18	17	fveq1d	$⊢ (φ \land (x \in Z \land z \in T)) \to (x \in Z ⟼ {A ↾}_{T}) (x) (z) = ({A ↾}_{T}) (z)$
19		eqid	$⊢ (x \in Z ⟼ A) = (x \in Z ⟼ A)$
20	19	fvmpt2	$⊢ (x \in Z \land A \in W) \to (x \in Z ⟼ A) (x) = A$
21	11 12 20	syl2anc	$⊢ (φ \land (x \in Z \land z \in T)) \to (x \in Z ⟼ A) (x) = A$
22	21	fveq1d	$⊢ (φ \land (x \in Z \land z \in T)) \to (x \in Z ⟼ A) (x) (z) = A (z)$
23	10 18 22	3eqtr4d	$⊢ (φ \land (x \in Z \land z \in T)) \to (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z)$
24	23	ralrimivva	$⊢ φ \to \forall x \in Z \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z)$
25		nfv	$⊢ Ⅎ k \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z)$
26		nfcv	$⊢ \underline{Ⅎ} x T$
27		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in Z ⟼ {A ↾}_{T}) (k)$
28		nfcv	$⊢ \underline{Ⅎ} x z$
29	27 28	nffv	$⊢ \underline{Ⅎ} x (x \in Z ⟼ {A ↾}_{T}) (k) (z)$
30		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in Z ⟼ A) (k)$
31	30 28	nffv	$⊢ \underline{Ⅎ} x (x \in Z ⟼ A) (k) (z)$
32	29 31	nfeq	$⊢ Ⅎ x (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z)$
33	26 32	nfralw	$⊢ Ⅎ x \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z)$
34		fveq2	$⊢ x = k \to (x \in Z ⟼ {A ↾}_{T}) (x) = (x \in Z ⟼ {A ↾}_{T}) (k)$
35	34	fveq1d	$⊢ x = k \to (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ {A ↾}_{T}) (k) (z)$
36		fveq2	$⊢ x = k \to (x \in Z ⟼ A) (x) = (x \in Z ⟼ A) (k)$
37	36	fveq1d	$⊢ x = k \to (x \in Z ⟼ A) (x) (z) = (x \in Z ⟼ A) (k) (z)$
38	35 37	eqeq12d	$⊢ x = k \to ((x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z) \leftrightarrow (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z))$
39	38	ralbidv	$⊢ x = k \to (\forall z \in T (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z) \leftrightarrow \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z))$
40	25 33 39	cbvralw	$⊢ \forall x \in Z \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (x) (z) = (x \in Z ⟼ A) (x) (z) \leftrightarrow \forall k \in Z \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z)$
41	24 40	sylib	$⊢ φ \to \forall k \in Z \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z)$
42	41	r19.21bi	$⊢ (φ \land k \in Z) \to \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z)$
43		fvoveq1	$⊢ (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z) \to \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| = \|(x \in Z ⟼ A) (k) (z) - G (z)\|$
44	43	breq1d	$⊢ (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z) \to (\|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r \leftrightarrow \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
45	44	ralimi	$⊢ \forall z \in T (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ A) (k) (z) \to \forall z \in T (\|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r \leftrightarrow \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
46		ralbi	$⊢ \forall z \in T (\|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r \leftrightarrow \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r) \to (\forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r \leftrightarrow \forall z \in T \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
47	42 45 46	3syl	$⊢ (φ \land k \in Z) \to (\forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r \leftrightarrow \forall z \in T \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
48	8 47	sylibrd	$⊢ (φ \land k \in Z) \to (\forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
49	5 48	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (\forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
50	49	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (\forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
51	50	ralimdva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall k \in ℤ_{\geq j} \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
52	51	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
53	52	ralimdv	$⊢ φ \to (\forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r \to \forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
54		ulmf	$⊢ (x \in Z ⟼ A) \underset{u}{⇝} (S) G \to \exists m \in ℤ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S}$
55	4 54	syl	$⊢ φ \to \exists m \in ℤ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S}$
56		fdm	$⊢ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to dom (x \in Z ⟼ A) = ℤ_{\geq m}$
57	19	dmmptss	$⊢ dom (x \in Z ⟼ A) \subseteq Z$
58	56 57	eqsstrrdi	$⊢ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to ℤ_{\geq m} \subseteq Z$
59		uzid	$⊢ m \in ℤ \to m \in ℤ_{\geq m}$
60	59	adantl	$⊢ (φ \land m \in ℤ) \to m \in ℤ_{\geq m}$
61		ssel	$⊢ ℤ_{\geq m} \subseteq Z \to (m \in ℤ_{\geq m} \to m \in Z)$
62		eluzel2	$⊢ m \in ℤ_{\geq M} \to M \in ℤ$
63	62 1	eleq2s	$⊢ m \in Z \to M \in ℤ$
64	61 63	syl6	$⊢ ℤ_{\geq m} \subseteq Z \to (m \in ℤ_{\geq m} \to M \in ℤ)$
65	58 60 64	syl2imc	$⊢ (φ \land m \in ℤ) \to ((x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to M \in ℤ)$
66	65	rexlimdva	$⊢ φ \to (\exists m \in ℤ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to M \in ℤ)$
67	55 66	mpd	$⊢ φ \to M \in ℤ$
68	3	ralrimiva	$⊢ φ \to \forall x \in Z A \in W$
69	19	fnmpt	$⊢ \forall x \in Z A \in W \to (x \in Z ⟼ A) Fn Z$
70	68 69	syl	$⊢ φ \to (x \in Z ⟼ A) Fn Z$
71		frn	$⊢ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to ran (x \in Z ⟼ A) \subseteq ℂ^{S}$
72	71	rexlimivw	$⊢ \exists m \in ℤ (x \in Z ⟼ A) : ℤ_{\geq m} ⟶ ℂ^{S} \to ran (x \in Z ⟼ A) \subseteq ℂ^{S}$
73	55 72	syl	$⊢ φ \to ran (x \in Z ⟼ A) \subseteq ℂ^{S}$
74		df-f	$⊢ (x \in Z ⟼ A) : Z ⟶ ℂ^{S} \leftrightarrow ((x \in Z ⟼ A) Fn Z \land ran (x \in Z ⟼ A) \subseteq ℂ^{S})$
75	70 73 74	sylanbrc	$⊢ φ \to (x \in Z ⟼ A) : Z ⟶ ℂ^{S}$
76		eqidd	$⊢ (φ \land (k \in Z \land z \in S)) \to (x \in Z ⟼ A) (k) (z) = (x \in Z ⟼ A) (k) (z)$
77		eqidd	$⊢ (φ \land z \in S) \to G (z) = G (z)$
78		ulmcl	$⊢ (x \in Z ⟼ A) \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
79	4 78	syl	$⊢ φ \to G : S ⟶ ℂ$
80		ulmscl	$⊢ (x \in Z ⟼ A) \underset{u}{⇝} (S) G \to S \in V$
81	4 80	syl	$⊢ φ \to S \in V$
82	1 67 75 76 77 79 81	ulm2	$⊢ φ \to ((x \in Z ⟼ A) \underset{u}{⇝} (S) G \leftrightarrow \forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|(x \in Z ⟼ A) (k) (z) - G (z)\| < r)$
83	75	fvmptelrn	$⊢ (φ \land x \in Z) \to A \in (ℂ^{S})$
84		elmapi	$⊢ A \in (ℂ^{S}) \to A : S ⟶ ℂ$
85	83 84	syl	$⊢ (φ \land x \in Z) \to A : S ⟶ ℂ$
86	2	adantr	$⊢ (φ \land x \in Z) \to T \subseteq S$
87	85 86	fssresd	$⊢ (φ \land x \in Z) \to ({A ↾}_{T}) : T ⟶ ℂ$
88		cnex	$⊢ ℂ \in V$
89	81 2	ssexd	$⊢ φ \to T \in V$
90	89	adantr	$⊢ (φ \land x \in Z) \to T \in V$
91		elmapg	$⊢ (ℂ \in V \land T \in V) \to ({A ↾}_{T} \in (ℂ^{T}) \leftrightarrow ({A ↾}_{T}) : T ⟶ ℂ)$
92	88 90 91	sylancr	$⊢ (φ \land x \in Z) \to ({A ↾}_{T} \in (ℂ^{T}) \leftrightarrow ({A ↾}_{T}) : T ⟶ ℂ)$
93	87 92	mpbird	$⊢ (φ \land x \in Z) \to {A ↾}_{T} \in (ℂ^{T})$
94	93	fmpttd	$⊢ φ \to (x \in Z ⟼ {A ↾}_{T}) : Z ⟶ ℂ^{T}$
95		eqidd	$⊢ (φ \land (k \in Z \land z \in T)) \to (x \in Z ⟼ {A ↾}_{T}) (k) (z) = (x \in Z ⟼ {A ↾}_{T}) (k) (z)$
96		fvres	$⊢ z \in T \to ({G ↾}_{T}) (z) = G (z)$
97	96	adantl	$⊢ (φ \land z \in T) \to ({G ↾}_{T}) (z) = G (z)$
98	79 2	fssresd	$⊢ φ \to ({G ↾}_{T}) : T ⟶ ℂ$
99	1 67 94 95 97 98 89	ulm2	$⊢ φ \to ((x \in Z ⟼ {A ↾}_{T}) \underset{u}{⇝} (T) ({G ↾}_{T}) \leftrightarrow \forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in T \|(x \in Z ⟼ {A ↾}_{T}) (k) (z) - G (z)\| < r)$
100	53 82 99	3imtr4d	$⊢ φ \to ((x \in Z ⟼ A) \underset{u}{⇝} (S) G \to (x \in Z ⟼ {A ↾}_{T}) \underset{u}{⇝} (T) ({G ↾}_{T}))$
101	4 100	mpd	$⊢ φ \to (x \in Z ⟼ {A ↾}_{T}) \underset{u}{⇝} (T) ({G ↾}_{T})$

Metamath Proof Explorer

Theorem ulmss

Proof