Theorem ulmdv

Description: If F is a sequence of differentiable functions on X which converge pointwise to G , and the derivatives of F ( n ) converge uniformly to H , then G is differentiable with derivative H . (Contributed by Mario Carneiro, 27-Feb-2015)

	Ref	Expression
Hypotheses	ulmdv.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	ulmdv.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	ulmdv.m	$$⊢\phi \to M\in \mathbb{Z}$$
	ulmdv.f	$$⊢\phi \to F:Z⟶{ℂ}^X$$
	ulmdv.g	$$⊢\phi \to G:X⟶ℂ$$
	ulmdv.l	$$⊢\left(\phi \wedge z\in X\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)⇝G\left(z\right)$$
	ulmdv.u	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H$$
Assertion	ulmdv	$$⊢\phi \to S\mathrm{D}G=H$$

Proof

Step	Hyp	Ref	Expression
1		ulmdv.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		ulmdv.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
3		ulmdv.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		ulmdv.f	$$⊢\phi \to F:Z⟶{ℂ}^X$$
5		ulmdv.g	$$⊢\phi \to G:X⟶ℂ$$
6		ulmdv.l	$$⊢\left(\phi \wedge z\in X\right)\to \left(k\in Z⟼F\left(k\right)\left(z\right)\right)⇝G\left(z\right)$$
7		ulmdv.u	$$⊢\phi \to \left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H$$
8		dvfg	$$⊢S\in \left\{ℝ,ℂ\right\}\to G_S^{\prime }:\mathrm{dom}{G}_S^{\prime }⟶ℂ$$
9	2 8	syl	$$⊢\phi \to G_S^{\prime }:\mathrm{dom}{G}_S^{\prime }⟶ℂ$$
10		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
11	2 10	syl	$$⊢\phi \to S\subseteq ℂ$$
12		biidd	$$⊢k=M\to \left(X\subseteq S\leftrightarrow X\subseteq S\right)$$
13	1 2 3 4 5 6 7	ulmdvlem2	$$⊢\left(\phi \wedge k\in Z\right)\to \mathrm{dom}{F\left(k\right)}_S^{\prime }=X$$
14		dvbsss	$$⊢\mathrm{dom}{F\left(k\right)}_S^{\prime }\subseteq S$$
15	13 14	eqsstrrdi	$$⊢\left(\phi \wedge k\in Z\right)\to X\subseteq S$$
16	15	ralrimiva	$$⊢\phi \to \forall k\in ZX\subseteq S$$
17		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
18	3 17	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
19	18 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
20	12 16 19	rspcdva	$$⊢\phi \to X\subseteq S$$
21	11 5 20	dvbss	$$⊢\phi \to \mathrm{dom}{G}_S^{\prime }\subseteq X$$
22	1 2 3 4 5 6 7	ulmdvlem3	$$⊢\left(\phi \wedge z\in X\right)\to z{G}_S^{\prime }H\left(z\right)$$
23		vex	$$⊢z\in \mathrm{V}$$
24		fvex	$$⊢H\left(z\right)\in \mathrm{V}$$
25	23 24	breldm	$$⊢z{G}_S^{\prime }H\left(z\right)\to z\in \mathrm{dom}{G}_S^{\prime }$$
26	22 25	syl	$$⊢\left(\phi \wedge z\in X\right)\to z\in \mathrm{dom}{G}_S^{\prime }$$
27	21 26	eqelssd	$$⊢\phi \to \mathrm{dom}{G}_S^{\prime }=X$$
28	27	feq2d	$$⊢\phi \to \left(G_S^{\prime }:\mathrm{dom}{G}_S^{\prime }⟶ℂ\leftrightarrow G_S^{\prime }:X⟶ℂ\right)$$
29	9 28	mpbid	$$⊢\phi \to G_S^{\prime }:X⟶ℂ$$
30	29	ffnd	$$⊢\phi \to G_S^{\prime }FnX$$
31		ulmcl	$$⊢\left(k\in Z⟼S\mathrm{D}F\left(k\right)\right)\underset{u}{⇝}\left(X\right)H\to H:X⟶ℂ$$
32	7 31	syl	$$⊢\phi \to H:X⟶ℂ$$
33	32	ffnd	$$⊢\phi \to HFnX$$
34	9	ffund	$$⊢\phi \to \mathrm{Fun}{G}_S^{\prime }$$
35	34	adantr	$$⊢\left(\phi \wedge z\in X\right)\to \mathrm{Fun}{G}_S^{\prime }$$
36		funbrfv	$$⊢\mathrm{Fun}{G}_S^{\prime }\to \left(z{G}_S^{\prime }H\left(z\right)\to G_S^{\prime }\left(z\right)=H\left(z\right)\right)$$
37	35 22 36	sylc	$$⊢\left(\phi \wedge z\in X\right)\to G_S^{\prime }\left(z\right)=H\left(z\right)$$
38	30 33 37	eqfnfvd	$$⊢\phi \to S\mathrm{D}G=H$$