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 
|- Z = ( ZZ>= ` M )
ulmdv.s 
|- ( ph -> S e. { RR , CC } )
ulmdv.m 
|- ( ph -> M e. ZZ )
ulmdv.f 
|- ( ph -> F : Z --> ( CC ^m X ) )
ulmdv.g 
|- ( ph -> G : X --> CC )
ulmdv.l 
|- ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
ulmdv.u 
|- ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H )
Assertion ulmdv 
|- ( ph -> ( S _D G ) = H )

Proof

Step Hyp Ref Expression
1 ulmdv.z 
 |-  Z = ( ZZ>= ` M )
2 ulmdv.s 
 |-  ( ph -> S e. { RR , CC } )
3 ulmdv.m 
 |-  ( ph -> M e. ZZ )
4 ulmdv.f 
 |-  ( ph -> F : Z --> ( CC ^m X ) )
5 ulmdv.g 
 |-  ( ph -> G : X --> CC )
6 ulmdv.l 
 |-  ( ( ph /\ z e. X ) -> ( k e. Z |-> ( ( F ` k ) ` z ) ) ~~> ( G ` z ) )
7 ulmdv.u 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H )
8 dvfg 
 |-  ( S e. { RR , CC } -> ( S _D G ) : dom ( S _D G ) --> CC )
9 2 8 syl 
 |-  ( ph -> ( S _D G ) : dom ( S _D G ) --> CC )
10 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
11 2 10 syl 
 |-  ( ph -> S C_ CC )
12 biidd 
 |-  ( k = M -> ( X C_ S <-> X C_ S ) )
13 1 2 3 4 5 6 7 ulmdvlem2 
 |-  ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )
14 dvbsss 
 |-  dom ( S _D ( F ` k ) ) C_ S
15 13 14 eqsstrrdi 
 |-  ( ( ph /\ k e. Z ) -> X C_ S )
16 15 ralrimiva 
 |-  ( ph -> A. k e. Z X C_ S )
17 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
18 3 17 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
19 18 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
20 12 16 19 rspcdva 
 |-  ( ph -> X C_ S )
21 11 5 20 dvbss 
 |-  ( ph -> dom ( S _D G ) C_ X )
22 1 2 3 4 5 6 7 ulmdvlem3 
 |-  ( ( ph /\ z e. X ) -> z ( S _D G ) ( H ` z ) )
23 vex 
 |-  z e. _V
24 fvex 
 |-  ( H ` z ) e. _V
25 23 24 breldm 
 |-  ( z ( S _D G ) ( H ` z ) -> z e. dom ( S _D G ) )
26 22 25 syl 
 |-  ( ( ph /\ z e. X ) -> z e. dom ( S _D G ) )
27 21 26 eqelssd 
 |-  ( ph -> dom ( S _D G ) = X )
28 27 feq2d 
 |-  ( ph -> ( ( S _D G ) : dom ( S _D G ) --> CC <-> ( S _D G ) : X --> CC ) )
29 9 28 mpbid 
 |-  ( ph -> ( S _D G ) : X --> CC )
30 29 ffnd 
 |-  ( ph -> ( S _D G ) Fn X )
31 ulmcl 
 |-  ( ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H -> H : X --> CC )
32 7 31 syl 
 |-  ( ph -> H : X --> CC )
33 32 ffnd 
 |-  ( ph -> H Fn X )
34 9 ffund 
 |-  ( ph -> Fun ( S _D G ) )
35 34 adantr 
 |-  ( ( ph /\ z e. X ) -> Fun ( S _D G ) )
36 funbrfv 
 |-  ( Fun ( S _D G ) -> ( z ( S _D G ) ( H ` z ) -> ( ( S _D G ) ` z ) = ( H ` z ) ) )
37 35 22 36 sylc 
 |-  ( ( ph /\ z e. X ) -> ( ( S _D G ) ` z ) = ( H ` z ) )
38 30 33 37 eqfnfvd 
 |-  ( ph -> ( S _D G ) = H )