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 )