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 = ℤ_{\geq M}$
	ulmdv.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	ulmdv.m	$⊢ φ \to M \in ℤ$
	ulmdv.f	$⊢ φ \to F : Z ⟶ ℂ^{X}$
	ulmdv.g	$⊢ φ \to G : X ⟶ ℂ$
	ulmdv.l	$⊢ (φ \land z \in X) \to (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
	ulmdv.u	$⊢ φ \to (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H$
Assertion	ulmdv	$⊢ φ \to S D G = H$

Proof

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

Metamath Proof Explorer

Theorem ulmdv

Proof