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