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

Metamath Proof Explorer

Theorem ulmdvlem2

Description: Lemma for ulmdv . (Contributed by Mario Carneiro, 8-May-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 ulmdvlem2 
|- ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )

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 ovex 
 |-  ( S _D ( F ` k ) ) e. _V
9 8 rgenw 
 |-  A. k e. Z ( S _D ( F ` k ) ) e. _V
10 eqid 
 |-  ( k e. Z |-> ( S _D ( F ` k ) ) ) = ( k e. Z |-> ( S _D ( F ` k ) ) )
11 10 fnmpt 
 |-  ( A. k e. Z ( S _D ( F ` k ) ) e. _V -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
12 9 11 mp1i 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z )
13 ulmf2 
 |-  ( ( ( k e. Z |-> ( S _D ( F ` k ) ) ) Fn Z /\ ( k e. Z |-> ( S _D ( F ` k ) ) ) ( ~~>u ` X ) H ) -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
14 12 7 13 syl2anc 
 |-  ( ph -> ( k e. Z |-> ( S _D ( F ` k ) ) ) : Z --> ( CC ^m X ) )
15 14 fvmptelcdm 
 |-  ( ( ph /\ k e. Z ) -> ( S _D ( F ` k ) ) e. ( CC ^m X ) )
16 elmapi 
 |-  ( ( S _D ( F ` k ) ) e. ( CC ^m X ) -> ( S _D ( F ` k ) ) : X --> CC )
17 fdm 
 |-  ( ( S _D ( F ` k ) ) : X --> CC -> dom ( S _D ( F ` k ) ) = X )
18 15 16 17 3syl 
 |-  ( ( ph /\ k e. Z ) -> dom ( S _D ( F ` k ) ) = X )