Metamath Proof Explorer

Theorem prdssca

Description: Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015) (Revised by Mario Carneiro, 15-Aug-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by Zhi Wang, 18-Aug-2024)

Ref Expression
Hypotheses prdsbas.p 
|- P = ( S Xs_ R )
prdsbas.s 
|- ( ph -> S e. V )
prdsbas.r 
|- ( ph -> R e. W )
Assertion prdssca 
|- ( ph -> S = ( Scalar ` P ) )

Proof

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 eqid 
 |-  ( Base ` S ) = ( Base ` S )
5 eqidd 
 |-  ( ph -> dom R = dom R )
6 eqidd 
 |-  ( ph -> X_ x e. dom R ( Base ` ( R ` x ) ) = X_ x e. dom R ( Base ` ( R ` x ) ) )
7 eqidd 
 |-  ( ph -> ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) )
8 eqidd 
 |-  ( ph -> ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
9 eqidd 
 |-  ( ph -> ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
10 eqidd 
 |-  ( ph -> ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) = ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) )
11 eqidd 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
12 eqidd 
 |-  ( ph -> { <. f , g >. | ( { f , g } C_ X_ x e. dom R ( Base ` ( R ` x ) ) /\ A. x e. dom R ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } = { <. f , g >. | ( { f , g } C_ X_ x e. dom R ( Base ` ( R ` x ) ) /\ A. x e. dom R ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
13 eqidd 
 |-  ( ph -> ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> sup ( ( ran ( x e. dom R |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) = ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> sup ( ( ran ( x e. dom R |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
14 eqidd 
 |-  ( ph -> ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) = ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )
15 eqidd 
 |-  ( ph -> ( a e. ( X_ x e. dom R ( Base ` ( R ` x ) ) X. X_ x e. dom R ( Base ` ( R ` x ) ) ) , c e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. dom R |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) = ( a e. ( X_ x e. dom R ( Base ` ( R ` x ) ) X. X_ x e. dom R ( Base ` ( R ` x ) ) ) , c e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. dom R |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) )
16 1 4 5 6 7 8 9 10 11 12 13 14 15 2 3 prdsval 
 |-  ( ph -> P = ( ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ X_ x e. dom R ( Base ` ( R ` x ) ) /\ A. x e. dom R ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> sup ( ( ran ( x e. dom R |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. dom R ( Base ` ( R ` x ) ) X. X_ x e. dom R ( Base ` ( R ` x ) ) ) , c e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. dom R |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) ) )
17 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
18 scaid 
 |-  Scalar = Slot ( Scalar ` ndx )
19 snsstp1 
 |-  { <. ( Scalar ` ndx ) , S >. } C_ { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. }
20 ssun2 
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
21 19 20 sstri 
 |-  { <. ( Scalar ` ndx ) , S >. } C_ ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } )
22 ssun1 
 |-  ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ X_ x e. dom R ( Base ` ( R ` x ) ) /\ A. x e. dom R ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> sup ( ( ran ( x e. dom R |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. dom R ( Base ` ( R ` x ) ) X. X_ x e. dom R ( Base ` ( R ` x ) ) ) , c e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. dom R |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
23 21 22 sstri 
 |-  { <. ( Scalar ` ndx ) , S >. } C_ ( ( { <. ( Base ` ndx ) , X_ x e. dom R ( Base ` ( R ` x ) ) >. , <. ( +g ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( +g ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .r ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. ( Base ` S ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( x e. dom R |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. , <. ( .i ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( S gsum ( x e. dom R |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( Xt_ ` ( TopOpen o. R ) ) >. , <. ( le ` ndx ) , { <. f , g >. | ( { f , g } C_ X_ x e. dom R ( Base ` ( R ` x ) ) /\ A. x e. dom R ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } >. , <. ( dist ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> sup ( ( ran ( x e. dom R |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) >. } u. { <. ( Hom ` ndx ) , ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. , <. ( comp ` ndx ) , ( a e. ( X_ x e. dom R ( Base ` ( R ` x ) ) X. X_ x e. dom R ( Base ` ( R ` x ) ) ) , c e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> ( d e. ( ( 2nd ` a ) ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) c ) , e e. ( ( f e. X_ x e. dom R ( Base ` ( R ` x ) ) , g e. X_ x e. dom R ( Base ` ( R ` x ) ) |-> X_ x e. dom R ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) ` a ) |-> ( x e. dom R |-> ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >. ( comp ` ( R ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >. } ) )
24 16 17 18 2 23 prdsvallem 
 |-  ( ph -> ( Scalar ` P ) = S )
25 24 eqcomd 
 |-  ( ph -> S = ( Scalar ` P ) )