Step |
Hyp |
Ref |
Expression |
1 |
|
psrplusg.s |
|- S = ( I mPwSer R ) |
2 |
|
psrplusg.b |
|- B = ( Base ` S ) |
3 |
|
psrplusg.a |
|- .+ = ( +g ` R ) |
4 |
|
psrplusg.p |
|- .+b = ( +g ` S ) |
5 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
6 |
|
eqid |
|- ( .r ` R ) = ( .r ` R ) |
7 |
|
eqid |
|- ( TopOpen ` R ) = ( TopOpen ` R ) |
8 |
|
eqid |
|- { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |
9 |
|
simpl |
|- ( ( I e. _V /\ R e. _V ) -> I e. _V ) |
10 |
1 5 8 2 9
|
psrbas |
|- ( ( I e. _V /\ R e. _V ) -> B = ( ( Base ` R ) ^m { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) ) |
11 |
|
eqid |
|- ( oF .+ |` ( B X. B ) ) = ( oF .+ |` ( B X. B ) ) |
12 |
|
eqid |
|- ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) = ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) |
13 |
|
eqid |
|- ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) = ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) |
14 |
|
eqidd |
|- ( ( I e. _V /\ R e. _V ) -> ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) = ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) ) |
15 |
|
simpr |
|- ( ( I e. _V /\ R e. _V ) -> R e. _V ) |
16 |
1 5 3 6 7 8 10 11 12 13 14 9 15
|
psrval |
|- ( ( I e. _V /\ R e. _V ) -> S = ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) |
17 |
16
|
fveq2d |
|- ( ( I e. _V /\ R e. _V ) -> ( +g ` S ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) ) |
18 |
2
|
fvexi |
|- B e. _V |
19 |
18 18
|
xpex |
|- ( B X. B ) e. _V |
20 |
|
ofexg |
|- ( ( B X. B ) e. _V -> ( oF .+ |` ( B X. B ) ) e. _V ) |
21 |
|
psrvalstr |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) Struct <. 1 , 9 >. |
22 |
|
plusgid |
|- +g = Slot ( +g ` ndx ) |
23 |
|
snsstp2 |
|- { <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } |
24 |
|
ssun1 |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) |
25 |
23 24
|
sstri |
|- { <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) |
26 |
21 22 25
|
strfv |
|- ( ( oF .+ |` ( B X. B ) ) e. _V -> ( oF .+ |` ( B X. B ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) ) |
27 |
19 20 26
|
mp2b |
|- ( oF .+ |` ( B X. B ) ) = ( +g ` ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( oF .+ |` ( B X. B ) ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( k e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> ( R gsum ( x e. { y e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } | y oR <_ k } |-> ( ( f ` x ) ( .r ` R ) ( g ` ( k oF - x ) ) ) ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , R >. , <. ( .s ` ndx ) , ( x e. ( Base ` R ) , f e. B |-> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { x } ) oF ( .r ` R ) f ) ) >. , <. ( TopSet ` ndx ) , ( Xt_ ` ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( TopOpen ` R ) } ) ) >. } ) ) |
28 |
17 4 27
|
3eqtr4g |
|- ( ( I e. _V /\ R e. _V ) -> .+b = ( oF .+ |` ( B X. B ) ) ) |
29 |
|
reldmpsr |
|- Rel dom mPwSer |
30 |
29
|
ovprc |
|- ( -. ( I e. _V /\ R e. _V ) -> ( I mPwSer R ) = (/) ) |
31 |
1 30
|
syl5eq |
|- ( -. ( I e. _V /\ R e. _V ) -> S = (/) ) |
32 |
31
|
fveq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( +g ` S ) = ( +g ` (/) ) ) |
33 |
22
|
str0 |
|- (/) = ( +g ` (/) ) |
34 |
32 4 33
|
3eqtr4g |
|- ( -. ( I e. _V /\ R e. _V ) -> .+b = (/) ) |
35 |
31
|
fveq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( Base ` S ) = ( Base ` (/) ) ) |
36 |
|
base0 |
|- (/) = ( Base ` (/) ) |
37 |
35 2 36
|
3eqtr4g |
|- ( -. ( I e. _V /\ R e. _V ) -> B = (/) ) |
38 |
37
|
xpeq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( B X. B ) = ( B X. (/) ) ) |
39 |
|
xp0 |
|- ( B X. (/) ) = (/) |
40 |
38 39
|
eqtrdi |
|- ( -. ( I e. _V /\ R e. _V ) -> ( B X. B ) = (/) ) |
41 |
40
|
reseq2d |
|- ( -. ( I e. _V /\ R e. _V ) -> ( oF .+ |` ( B X. B ) ) = ( oF .+ |` (/) ) ) |
42 |
|
res0 |
|- ( oF .+ |` (/) ) = (/) |
43 |
41 42
|
eqtrdi |
|- ( -. ( I e. _V /\ R e. _V ) -> ( oF .+ |` ( B X. B ) ) = (/) ) |
44 |
34 43
|
eqtr4d |
|- ( -. ( I e. _V /\ R e. _V ) -> .+b = ( oF .+ |` ( B X. B ) ) ) |
45 |
28 44
|
pm2.61i |
|- .+b = ( oF .+ |` ( B X. B ) ) |