Step |
Hyp |
Ref |
Expression |
1 |
|
psrvsca.s |
|- S = ( I mPwSer R ) |
2 |
|
psrvsca.n |
|- .xb = ( .s ` S ) |
3 |
|
psrvsca.k |
|- K = ( Base ` R ) |
4 |
|
psrvsca.b |
|- B = ( Base ` S ) |
5 |
|
psrvsca.m |
|- .x. = ( .r ` R ) |
6 |
|
psrvsca.d |
|- D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
7 |
|
eqid |
|- ( +g ` R ) = ( +g ` R ) |
8 |
|
eqid |
|- ( TopOpen ` R ) = ( TopOpen ` R ) |
9 |
|
simpl |
|- ( ( I e. _V /\ R e. _V ) -> I e. _V ) |
10 |
1 3 6 4 9
|
psrbas |
|- ( ( I e. _V /\ R e. _V ) -> B = ( K ^m D ) ) |
11 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
12 |
1 4 7 11
|
psrplusg |
|- ( +g ` S ) = ( oF ( +g ` R ) |` ( B X. B ) ) |
13 |
|
eqid |
|- ( .r ` S ) = ( .r ` S ) |
14 |
1 4 5 13 6
|
psrmulr |
|- ( .r ` S ) = ( f e. B , g e. B |-> ( k e. D |-> ( R gsum ( x e. { y e. D | y oR <_ k } |-> ( ( f ` x ) .x. ( g ` ( k oF - x ) ) ) ) ) ) ) |
15 |
|
eqid |
|- ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) |
16 |
|
eqidd |
|- ( ( I e. _V /\ R e. _V ) -> ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) ) |
17 |
|
simpr |
|- ( ( I e. _V /\ R e. _V ) -> R e. _V ) |
18 |
1 3 7 5 8 6 10 12 14 15 16 9 17
|
psrval |
|- ( ( I e. _V /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) |
19 |
18
|
fveq2d |
|- ( ( I e. _V /\ R e. _V ) -> ( .s ` S ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) ) |
20 |
3
|
fvexi |
|- K e. _V |
21 |
4
|
fvexi |
|- B e. _V |
22 |
20 21
|
mpoex |
|- ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) e. _V |
23 |
|
psrvalstr |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >. |
24 |
|
vscaid |
|- .s = Slot ( .s ` ndx ) |
25 |
|
snsstp2 |
|- { <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. } C_ { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } |
26 |
|
ssun2 |
|- { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) |
27 |
25 26
|
sstri |
|- { <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) |
28 |
23 24 27
|
strfv |
|- ( ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) e. _V -> ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) ) |
29 |
22 28
|
ax-mp |
|- ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( .s ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` S ) >. , <. ( .r ` ndx ) , ( .r ` S ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( D X. { ( TopOpen ` R ) } ) ) >. } ) ) |
30 |
19 2 29
|
3eqtr4g |
|- ( ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) ) |
31 |
|
eqid |
|- (/) = (/) |
32 |
|
fn0 |
|- ( (/) Fn (/) <-> (/) = (/) ) |
33 |
31 32
|
mpbir |
|- (/) Fn (/) |
34 |
|
reldmpsr |
|- Rel dom mPwSer |
35 |
34
|
ovprc |
|- ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) ) |
36 |
1 35
|
syl5eq |
|- ( -. ( I e. _V /\ R e. _V ) -> S = (/) ) |
37 |
36
|
fveq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( .s ` S ) = ( .s ` (/) ) ) |
38 |
|
df-vsca |
|- .s = Slot 6 |
39 |
38
|
str0 |
|- (/) = ( .s ` (/) ) |
40 |
37 2 39
|
3eqtr4g |
|- ( -. ( I e. _V /\ R e. _V ) -> .xb = (/) ) |
41 |
34 1 4
|
elbasov |
|- ( f e. B -> ( I e. _V /\ R e. _V ) ) |
42 |
41
|
con3i |
|- ( -. ( I e. _V /\ R e. _V ) -> -. f e. B ) |
43 |
42
|
eq0rdv |
|- ( -. ( I e. _V /\ R e. _V ) -> B = (/) ) |
44 |
43
|
xpeq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( K X. B ) = ( K X. (/) ) ) |
45 |
|
xp0 |
|- ( K X. (/) ) = (/) |
46 |
44 45
|
eqtrdi |
|- ( -. ( I e. _V /\ R e. _V ) -> ( K X. B ) = (/) ) |
47 |
40 46
|
fneq12d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( .xb Fn ( K X. B ) <-> (/) Fn (/) ) ) |
48 |
33 47
|
mpbiri |
|- ( -. ( I e. _V /\ R e. _V ) -> .xb Fn ( K X. B ) ) |
49 |
|
fnov |
|- ( .xb Fn ( K X. B ) <-> .xb = ( x e. K , f e. B |-> ( x .xb f ) ) ) |
50 |
48 49
|
sylib |
|- ( -. ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( x .xb f ) ) ) |
51 |
42
|
pm2.21d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( f e. B -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) ) ) |
52 |
51
|
a1d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( x e. K -> ( f e. B -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) ) ) ) |
53 |
52
|
3imp |
|- ( ( -. ( I e. _V /\ R e. _V ) /\ x e. K /\ f e. B ) -> ( ( D X. { x } ) oF .x. f ) = ( x .xb f ) ) |
54 |
53
|
mpoeq3dva |
|- ( -. ( I e. _V /\ R e. _V ) -> ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) = ( x e. K , f e. B |-> ( x .xb f ) ) ) |
55 |
50 54
|
eqtr4d |
|- ( -. ( I e. _V /\ R e. _V ) -> .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) ) |
56 |
30 55
|
pm2.61i |
|- .xb = ( x e. K , f e. B |-> ( ( D X. { x } ) oF .x. f ) ) |