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	fvmptelrn	|- ( ( 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 )