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