This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) = 𝐻 )