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 |
|
imasmulr.p |
|- .x. = ( .r ` R ) |
6 |
|
imasmulr.t |
|- .xb = ( .r ` U ) |
7 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
8 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
9 |
|
eqid |
|- ( Base ` ( Scalar ` R ) ) = ( Base ` ( Scalar ` R ) ) |
10 |
|
eqid |
|- ( .s ` R ) = ( .s ` R ) |
11 |
|
eqid |
|- ( .i ` R ) = ( .i ` R ) |
12 |
|
eqid |
|- ( TopOpen ` R ) = ( TopOpen ` R ) |
13 |
|
eqid |
|- ( dist ` R ) = ( dist ` R ) |
14 |
|
eqid |
|- ( le ` R ) = ( le ` 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 |
|
eqidd |
|- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) |
18 |
|
eqidd |
|- ( ph -> U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) = U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) ) |
19 |
|
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 ) >. } ) |
20 |
|
eqidd |
|- ( ph -> ( ( TopOpen ` R ) qTop F ) = ( ( TopOpen ` R ) qTop F ) ) |
21 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
22 |
1 2 3 4 13 21
|
imasds |
|- ( ph -> ( dist ` U ) = ( x e. B , y e. B |-> inf ( U_ n e. NN ran ( g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = x /\ ( F ` ( 2nd ` ( h ` n ) ) ) = y /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } |-> ( RR*s gsum ( ( dist ` R ) o. g ) ) ) , RR* , < ) ) ) |
23 |
|
eqidd |
|- ( ph -> ( ( F o. ( le ` R ) ) o. `' F ) = ( ( F o. ( le ` R ) ) o. `' F ) ) |
24 |
1 2 7 5 8 9 10 11 12 13 14 16 17 18 19 20 22 23 3 4
|
imasval |
|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) ) |
25 |
|
eqid |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
26 |
25
|
imasvalstr |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) Struct <. 1 , ; 1 2 >. |
27 |
|
mulrid |
|- .r = Slot ( .r ` ndx ) |
28 |
|
snsstp3 |
|- { <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } |
29 |
|
ssun1 |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) |
30 |
28 29
|
sstri |
|- { <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) |
31 |
|
ssun1 |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
32 |
30 31
|
sstri |
|- { <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. ( Base ` ( Scalar ` R ) ) , x e. { ( F ` q ) } |-> ( F ` ( p ( .s ` R ) q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) u. { <. ( TopSet ` ndx ) , ( ( TopOpen ` R ) qTop F ) >. , <. ( le ` ndx ) , ( ( F o. ( le ` R ) ) o. `' F ) >. , <. ( dist ` ndx ) , ( dist ` U ) >. } ) |
33 |
|
fvex |
|- ( Base ` R ) e. _V |
34 |
2 33
|
eqeltrdi |
|- ( ph -> V e. _V ) |
35 |
|
snex |
|- { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V |
36 |
35
|
rgenw |
|- A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V |
37 |
|
iunexg |
|- ( ( V e. _V /\ A. q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) |
38 |
34 36 37
|
sylancl |
|- ( ph -> U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) |
39 |
38
|
ralrimivw |
|- ( ph -> A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) |
40 |
|
iunexg |
|- ( ( V e. _V /\ A. p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) |
41 |
34 39 40
|
syl2anc |
|- ( ph -> U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } e. _V ) |
42 |
24 26 27 32 41 6
|
strfv3 |
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } ) |