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 |
|
imassca.g |
|- G = ( Scalar ` R ) |
6 |
|
imasvsca.k |
|- K = ( Base ` G ) |
7 |
|
imasvsca.q |
|- .x. = ( .s ` R ) |
8 |
|
imasvsca.s |
|- .xb = ( .s ` U ) |
9 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
10 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
11 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
12 |
5
|
fveq2i |
|- ( Base ` G ) = ( Base ` ( Scalar ` R ) ) |
13 |
6 12
|
eqtri |
|- K = ( Base ` ( Scalar ` R ) ) |
14 |
|
eqid |
|- ( .i ` R ) = ( .i ` R ) |
15 |
|
eqid |
|- ( TopOpen ` R ) = ( TopOpen ` R ) |
16 |
|
eqid |
|- ( dist ` R ) = ( dist ` R ) |
17 |
|
eqid |
|- ( le ` R ) = ( le ` R ) |
18 |
|
eqid |
|- ( +g ` U ) = ( +g ` U ) |
19 |
1 2 3 4 9 18
|
imasplusg |
|- ( ph -> ( +g ` U ) = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p ( +g ` R ) q ) ) >. } ) |
20 |
|
eqid |
|- ( .r ` U ) = ( .r ` U ) |
21 |
1 2 3 4 10 20
|
imasmulr |
|- ( ph -> ( .r ` U ) = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p ( .r ` R ) q ) ) >. } ) |
22 |
|
eqidd |
|- ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) |
23 |
|
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 ) >. } ) |
24 |
|
eqidd |
|- ( ph -> ( ( TopOpen ` R ) qTop F ) = ( ( TopOpen ` R ) qTop F ) ) |
25 |
|
eqid |
|- ( dist ` U ) = ( dist ` U ) |
26 |
1 2 3 4 16 25
|
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* , < ) ) ) |
27 |
|
eqidd |
|- ( ph -> ( ( F o. ( le ` R ) ) o. `' F ) = ( ( F o. ( le ` R ) ) o. `' F ) ) |
28 |
1 2 9 10 11 13 7 14 15 16 17 19 21 22 23 24 26 27 3 4
|
imasval |
|- ( ph -> U = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) >. } ) ) |
29 |
|
eqid |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) >. } ) |
30 |
29
|
imasvalstr |
|- ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 >. |
31 |
|
vscaid |
|- .s = Slot ( .s ` ndx ) |
32 |
|
snsstp2 |
|- { <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) >. } C_ { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } |
33 |
|
ssun2 |
|- { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) >. , <. ( .i ` ndx ) , U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( p ( .i ` R ) q ) >. } >. } ) |
34 |
|
ssun1 |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) >. } ) |
35 |
33 34
|
sstri |
|- { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) >. } ) |
36 |
32 35
|
sstri |
|- { <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` U ) >. , <. ( .r ` ndx ) , ( .r ` U ) >. } u. { <. ( Scalar ` ndx ) , ( Scalar ` R ) >. , <. ( .s ` ndx ) , U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. 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 ) >. } ) |
37 |
|
fvex |
|- ( Base ` R ) e. _V |
38 |
2 37
|
eqeltrdi |
|- ( ph -> V e. _V ) |
39 |
6
|
fvexi |
|- K e. _V |
40 |
|
snex |
|- { ( F ` q ) } e. _V |
41 |
39 40
|
mpoex |
|- ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) e. _V |
42 |
41
|
rgenw |
|- A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) e. _V |
43 |
|
iunexg |
|- ( ( V e. _V /\ A. q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) e. _V ) -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) e. _V ) |
44 |
38 42 43
|
sylancl |
|- ( ph -> U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) e. _V ) |
45 |
28 30 31 36 44 8
|
strfv3 |
|- ( ph -> .xb = U_ q e. V ( p e. K , x e. { ( F ` q ) } |-> ( F ` ( p .x. q ) ) ) ) |