Step |
Hyp |
Ref |
Expression |
1 |
|
prdsbas.p |
|- P = ( S Xs_ R ) |
2 |
|
prdsbas.s |
|- ( ph -> S e. V ) |
3 |
|
prdsbas.r |
|- ( ph -> R e. W ) |
4 |
|
prdsbas.b |
|- B = ( Base ` P ) |
5 |
|
prdsbas.i |
|- ( ph -> dom R = I ) |
6 |
|
prdsmulr.t |
|- .x. = ( .r ` P ) |
7 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
8 |
1 2 3 4 5
|
prdsbas |
|- ( ph -> B = X_ x e. I ( Base ` ( R ` x ) ) ) |
9 |
|
eqid |
|- ( +g ` P ) = ( +g ` P ) |
10 |
1 2 3 4 5 9
|
prdsplusg |
|- ( ph -> ( +g ` P ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) ) |
11 |
|
eqidd |
|- ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) ) |
12 |
|
eqidd |
|- ( ph -> ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) ) |
13 |
|
eqidd |
|- ( ph -> ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) = ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) ) |
14 |
|
eqidd |
|- ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) ) |
15 |
|
eqidd |
|- ( ph -> { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } ) |
16 |
|
eqidd |
|- ( ph -> ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) ) |
17 |
|
eqidd |
|- ( ph -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ) |
18 |
|
eqidd |
|- ( ph -> ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) ) |
19 |
1 7 5 8 10 11 12 13 14 15 16 17 18 2 3
|
prdsval |
|- ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) ) |
20 |
|
mulrid |
|- .r = Slot ( .r ` ndx ) |
21 |
|
ovssunirn |
|- ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) C_ U. ran ( .r ` ( R ` x ) ) |
22 |
20
|
strfvss |
|- ( .r ` ( R ` x ) ) C_ U. ran ( R ` x ) |
23 |
|
fvssunirn |
|- ( R ` x ) C_ U. ran R |
24 |
|
rnss |
|- ( ( R ` x ) C_ U. ran R -> ran ( R ` x ) C_ ran U. ran R ) |
25 |
|
uniss |
|- ( ran ( R ` x ) C_ ran U. ran R -> U. ran ( R ` x ) C_ U. ran U. ran R ) |
26 |
23 24 25
|
mp2b |
|- U. ran ( R ` x ) C_ U. ran U. ran R |
27 |
22 26
|
sstri |
|- ( .r ` ( R ` x ) ) C_ U. ran U. ran R |
28 |
|
rnss |
|- ( ( .r ` ( R ` x ) ) C_ U. ran U. ran R -> ran ( .r ` ( R ` x ) ) C_ ran U. ran U. ran R ) |
29 |
|
uniss |
|- ( ran ( .r ` ( R ` x ) ) C_ ran U. ran U. ran R -> U. ran ( .r ` ( R ` x ) ) C_ U. ran U. ran U. ran R ) |
30 |
27 28 29
|
mp2b |
|- U. ran ( .r ` ( R ` x ) ) C_ U. ran U. ran U. ran R |
31 |
21 30
|
sstri |
|- ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R |
32 |
|
ovex |
|- ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) e. _V |
33 |
32
|
elpw |
|- ( ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R <-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R ) |
34 |
31 33
|
mpbir |
|- ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R |
35 |
34
|
a1i |
|- ( ( ph /\ x e. I ) -> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R ) |
36 |
35
|
fmpttd |
|- ( ph -> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R ) |
37 |
|
rnexg |
|- ( R e. W -> ran R e. _V ) |
38 |
|
uniexg |
|- ( ran R e. _V -> U. ran R e. _V ) |
39 |
3 37 38
|
3syl |
|- ( ph -> U. ran R e. _V ) |
40 |
|
rnexg |
|- ( U. ran R e. _V -> ran U. ran R e. _V ) |
41 |
|
uniexg |
|- ( ran U. ran R e. _V -> U. ran U. ran R e. _V ) |
42 |
39 40 41
|
3syl |
|- ( ph -> U. ran U. ran R e. _V ) |
43 |
|
rnexg |
|- ( U. ran U. ran R e. _V -> ran U. ran U. ran R e. _V ) |
44 |
|
uniexg |
|- ( ran U. ran U. ran R e. _V -> U. ran U. ran U. ran R e. _V ) |
45 |
42 43 44
|
3syl |
|- ( ph -> U. ran U. ran U. ran R e. _V ) |
46 |
45
|
pwexd |
|- ( ph -> ~P U. ran U. ran U. ran R e. _V ) |
47 |
3
|
dmexd |
|- ( ph -> dom R e. _V ) |
48 |
5 47
|
eqeltrrd |
|- ( ph -> I e. _V ) |
49 |
46 48
|
elmapd |
|- ( ph -> ( ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R ) ) |
50 |
36 49
|
mpbird |
|- ( ph -> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) ) |
51 |
50
|
ralrimivw |
|- ( ph -> A. g e. B ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) ) |
52 |
51
|
ralrimivw |
|- ( ph -> A. f e. B A. g e. B ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) ) |
53 |
|
eqid |
|- ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) |
54 |
53
|
fmpo |
|- ( A. f e. B A. g e. B ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) ) |
55 |
52 54
|
sylib |
|- ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) ) |
56 |
4
|
fvexi |
|- B e. _V |
57 |
56 56
|
xpex |
|- ( B X. B ) e. _V |
58 |
|
ovex |
|- ( ~P U. ran U. ran U. ran R ^m I ) e. _V |
59 |
|
fex2 |
|- ( ( ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) /\ ( B X. B ) e. _V /\ ( ~P U. ran U. ran U. ran R ^m I ) e. _V ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V ) |
60 |
57 58 59
|
mp3an23 |
|- ( ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) : ( B X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V ) |
61 |
55 60
|
syl |
|- ( ph -> ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V ) |
62 |
|
snsstp3 |
|- { <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } |
63 |
|
ssun1 |
|- { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) |
64 |
62 63
|
sstri |
|- { <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) |
65 |
|
ssun1 |
|- ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) |
66 |
64 65
|
sstri |
|- { <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( B X. B ) , c e. B |-> ( d e. ( ( 2nd ` a ) ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. I |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) |
67 |
19 6 20 61 66
|
prdsbaslem |
|- ( ph -> .x. = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) ) |