Theorem ulmclm

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

	Ref	Expression
Hypotheses	ulmclm.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	ulmclm.m	$$⊢\phi \to M\in \mathbb{Z}$$
	ulmclm.f	$$⊢\phi \to F:Z⟶{ℂ}^S$$
	ulmclm.a	$$⊢\phi \to A\in S$$
	ulmclm.h	$$⊢\phi \to H\in W$$
	ulmclm.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\left(A\right)=H\left(k\right)$$
	ulmclm.u	$$⊢\phi \to F\underset{u}{⇝}\left(S\right)G$$
Assertion	ulmclm	$$⊢\phi \to H⇝G\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ulmclm.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ulmclm.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		ulmclm.f	$$⊢\phi \to F:Z⟶{ℂ}^S$$
4		ulmclm.a	$$⊢\phi \to A\in S$$
5		ulmclm.h	$$⊢\phi \to H\in W$$
6		ulmclm.e	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\left(A\right)=H\left(k\right)$$
7		ulmclm.u	$$⊢\phi \to F\underset{u}{⇝}\left(S\right)G$$
8		fveq2	$$⊢z=A\to F\left(k\right)\left(z\right)=F\left(k\right)\left(A\right)$$
9		fveq2	$$⊢z=A\to G\left(z\right)=G\left(A\right)$$
10	8 9	oveq12d	$$⊢z=A\to F\left(k\right)\left(z\right)-G\left(z\right)=F\left(k\right)\left(A\right)-G\left(A\right)$$
11	10	fveq2d	$$⊢z=A\to \left|F\left(k\right)\left(z\right)-G\left(z\right)\right|=\left|F\left(k\right)\left(A\right)-G\left(A\right)\right|$$
12	11	breq1d	$$⊢z=A\to \left(\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\leftrightarrow \left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
13	12	rspcv	$$⊢A\in S\to \left(\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\to \left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
14	4 13	syl	$$⊢\phi \to \left(\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\to \left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
15	14	ralimdv	$$⊢\phi \to \left(\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\to \forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
16	15	reximdv	$$⊢\phi \to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\to \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
17	16	ralimdv	$$⊢\phi \to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\to \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
18		eqidd	$$⊢\left(\phi \wedge \left(k\in Z\wedge z\in S\right)\right)\to F\left(k\right)\left(z\right)=F\left(k\right)\left(z\right)$$
19		eqidd	$$⊢\left(\phi \wedge z\in S\right)\to G\left(z\right)=G\left(z\right)$$
20		ulmcl	$$⊢F\underset{u}{⇝}\left(S\right)G\to G:S⟶ℂ$$
21	7 20	syl	$$⊢\phi \to G:S⟶ℂ$$
22		ulmscl	$$⊢F\underset{u}{⇝}\left(S\right)G\to S\in \mathrm{V}$$
23	7 22	syl	$$⊢\phi \to S\in \mathrm{V}$$
24	1 2 3 18 19 21 23	ulm2	$$⊢\phi \to \left(F\underset{u}{⇝}\left(S\right)G\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\forall z\in S\left|F\left(k\right)\left(z\right)-G\left(z\right)\right|<x\right)$$
25	6	eqcomd	$$⊢\left(\phi \wedge k\in Z\right)\to H\left(k\right)=F\left(k\right)\left(A\right)$$
26	21 4	ffvelcdmd	$$⊢\phi \to G\left(A\right)\in ℂ$$
27	3	ffvelcdmda	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in \left({ℂ}^S\right)$$
28		elmapi	$$⊢F\left(k\right)\in \left({ℂ}^S\right)\to F\left(k\right):S⟶ℂ$$
29	27 28	syl	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right):S⟶ℂ$$
30	4	adantr	$$⊢\left(\phi \wedge k\in Z\right)\to A\in S$$
31	29 30	ffvelcdmd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\left(A\right)\in ℂ$$
32	1 2 5 25 26 31	clim2c	$$⊢\phi \to \left(H⇝G\left(A\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left|F\left(k\right)\left(A\right)-G\left(A\right)\right|<x\right)$$
33	17 24 32	3imtr4d	$$⊢\phi \to \left(F\underset{u}{⇝}\left(S\right)G\to H⇝G\left(A\right)\right)$$
34	7 33	mpd	$$⊢\phi \to H⇝G\left(A\right)$$