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

Metamath Proof Explorer

Theorem ulmss

Proof