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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	ulmdv.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	ulmdv.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	ulmdv.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
	ulmdv.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
	ulmdv.l	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
	ulmdv.u	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
Assertion	ulmdv	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = 𝐻 )

Proof

Step	Hyp	Ref	Expression
1		ulmdv.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		ulmdv.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3		ulmdv.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4		ulmdv.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑋 ) )
5		ulmdv.g	⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ℂ )
6		ulmdv.l	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑘 ∈ 𝑍 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑧 ) ) ⇝ ( 𝐺 ‘ 𝑧 ) )
7		ulmdv.u	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 )
8		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
9	2 8	syl	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ )
10		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
11	2 10	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
12		biidd	⊢ ( 𝑘 = 𝑀 → ( 𝑋 ⊆ 𝑆 ↔ 𝑋 ⊆ 𝑆 ) )
13	1 2 3 4 5 6 7	ulmdvlem2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) = 𝑋 )
14		dvbsss	⊢ dom ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ⊆ 𝑆
15	13 14	eqsstrrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑋 ⊆ 𝑆 )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 𝑋 ⊆ 𝑆 )
17		uzid	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
18	3 17	syl	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
19	18 1	eleqtrrdi	⊢ ( 𝜑 → 𝑀 ∈ 𝑍 )
20	12 16 19	rspcdva	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
21	11 5 20	dvbss	⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) ⊆ 𝑋 )
22	1 2 3 4 5 6 7	ulmdvlem3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) )
23		vex	⊢ 𝑧 ∈ V
24		fvex	⊢ ( 𝐻 ‘ 𝑧 ) ∈ V
25	23 24	breldm	⊢ ( 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) → 𝑧 ∈ dom ( 𝑆 D 𝐺 ) )
26	22 25	syl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ dom ( 𝑆 D 𝐺 ) )
27	21 26	eqelssd	⊢ ( 𝜑 → dom ( 𝑆 D 𝐺 ) = 𝑋 )
28	27	feq2d	⊢ ( 𝜑 → ( ( 𝑆 D 𝐺 ) : dom ( 𝑆 D 𝐺 ) ⟶ ℂ ↔ ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ ) )
29	9 28	mpbid	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) : 𝑋 ⟶ ℂ )
30	29	ffnd	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) Fn 𝑋 )
31		ulmcl	⊢ ( ( 𝑘 ∈ 𝑍 ↦ ( 𝑆 D ( 𝐹 ‘ 𝑘 ) ) ) ( ⇝𝑢 ‘ 𝑋 ) 𝐻 → 𝐻 : 𝑋 ⟶ ℂ )
32	7 31	syl	⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ℂ )
33	32	ffnd	⊢ ( 𝜑 → 𝐻 Fn 𝑋 )
34	9	ffund	⊢ ( 𝜑 → Fun ( 𝑆 D 𝐺 ) )
35	34	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → Fun ( 𝑆 D 𝐺 ) )
36		funbrfv	⊢ ( Fun ( 𝑆 D 𝐺 ) → ( 𝑧 ( 𝑆 D 𝐺 ) ( 𝐻 ‘ 𝑧 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) ) )
37	35 22 36	sylc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑆 D 𝐺 ) ‘ 𝑧 ) = ( 𝐻 ‘ 𝑧 ) )
38	30 33 37	eqfnfvd	⊢ ( 𝜑 → ( 𝑆 D 𝐺 ) = 𝐻 )