Step |
Hyp |
Ref |
Expression |
1 |
|
imasbas.u |
|- ( ph -> U = ( F "s R ) ) |
2 |
|
imasbas.v |
|- ( ph -> V = ( Base ` R ) ) |
3 |
|
imasbas.f |
|- ( ph -> F : V -onto-> B ) |
4 |
|
imasbas.r |
|- ( ph -> R e. Z ) |
5 |
|
imasle.n |
|- N = ( le ` R ) |
6 |
|
imasle.l |
|- .<_ = ( le ` U ) |
7 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
8 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
9 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
10 |
|
eqid |
|- ( Base ` ( Scalar ` R ) ) = ( Base ` ( Scalar ` R ) ) |
11 |
|
eqid |
|- ( .s ` R ) = ( .s ` R ) |
12 |
|
eqid |
|- ( .i ` R ) = ( .i ` R ) |
13 |
|
eqid |
|- ( TopOpen ` R ) = ( TopOpen ` R ) |
14 |
|
eqid |
|- ( dist ` R ) = ( dist ` R ) |
15 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
16 |
1 2 3 4 7 15
|
imasplusg |
|- ( ph -> ( +g ` U ) = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p ( +g ` R ) q ) ) >. } ) |
17 |
|
eqid |
|- ( .r ` U ) = ( .r ` U ) |
18 |
1 2 3 4 8 17
|
imasmulr |
|- ( ph -> ( .r ` U ) = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p ( .r ` R ) q ) ) >. } ) |
19 |
|
eqid |
|- ( .s ` U ) = ( .s ` U ) |
20 |
1 2 3 4 9 10 11 19
|
imasvsca |
|- ( ph -> ( .s ` U ) = U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) ) |
21 |
|
eqidd |
|- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } ) |
22 |
|
eqid |
|- ( TopSet ` U ) = ( TopSet ` U ) |
23 |
1 2 3 4 13 22
|
imastset |
|- ( ph -> ( TopSet ` U ) = ( ( TopOpen ` R ) qTop F ) ) |
24 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
25 |
1 2 3 4 14 24
|
imasds |
|- ( ph -> ( dist ` U ) = ( x e. B , y e. B |-> inf ( U_ u e. NN ran ( z e. { w e. ( ( V X. V ) ^m ( 1 ... u ) ) | ( ( F ` ( 1st ` ( w ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( w ` u ) ) ) = y /\ A. v e. ( 1 ... ( u - 1 ) ) ( F ` ( 2nd ` ( w ` v ) ) ) = ( F ` ( 1st ` ( w ` ( v + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` R ) o. z ) ) ) , RR* , < ) ) ) |
26 |
|
eqidd |
|- ( ph -> ( ( F o. N ) o. `' F ) = ( ( F o. N ) o. `' F ) ) |
27 |
1 2 7 8 9 10 11 12 13 14 5 16 18 20 21 23 25 26 3 4
|
imasval |
|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) ) |
28 |
|
eqid |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
29 |
28
|
imasvalstr |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) Struct <. 1 , ; 1 2 >. |
30 |
|
pleid |
|- le = Slot ( le ` ndx ) |
31 |
|
snsstp2 |
|- { <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. } C_ { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } |
32 |
|
ssun2 |
|- { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
33 |
31 32
|
sstri |
|- { <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , ( .s ` U ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( TopSet ` U ) >. , <. ( le ` ndx ) , ( ( F o. N ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
34 |
|
fof |
|- ( F : V -onto-> B -> F : V --> B ) |
35 |
3 34
|
syl |
|- ( ph -> F : V --> B ) |
36 |
|
fvex |
|- ( Base ` R ) e. _V |
37 |
2 36
|
eqeltrdi |
|- ( ph -> V e. _V ) |
38 |
35 37
|
fexd |
|- ( ph -> F e. _V ) |
39 |
5
|
fvexi |
|- N e. _V |
40 |
|
coexg |
|- ( ( F e. _V /\ N e. _V ) -> ( F o. N ) e. _V ) |
41 |
38 39 40
|
sylancl |
|- ( ph -> ( F o. N ) e. _V ) |
42 |
|
cnvexg |
|- ( F e. _V -> `' F e. _V ) |
43 |
38 42
|
syl |
|- ( ph -> `' F e. _V ) |
44 |
|
coexg |
|- ( ( ( F o. N ) e. _V /\ `' F e. _V ) -> ( ( F o. N ) o. `' F ) e. _V ) |
45 |
41 43 44
|
syl2anc |
|- ( ph -> ( ( F o. N ) o. `' F ) e. _V ) |
46 |
27 29 30 33 45 6
|
strfv3 |
|- ( ph -> .<_ = ( ( F o. N ) o. `' F ) ) |