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 = ( ZZ>= ` M )
	ulmss.t	\|- ( ph -> T C_ S )
	ulmss.a	\|- ( ( ph /\ x e. Z ) -> A e. W )
	ulmss.u	\|- ( ph -> ( x e. Z \|-> A ) ( ~~>u ` S ) G )
Assertion	ulmss	\|- ( ph -> ( x e. Z \|-> ( A \|` T ) ) ( ~~>u ` T ) ( G \|` T ) )

Proof

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

Metamath Proof Explorer

Theorem ulmss

Proof