Metamath Proof Explorer

Theorem prdsvsca

Description: Scalar multiplication in 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 )
prdsbas.b 
|- B = ( Base ` P )
prdsbas.i 
|- ( ph -> dom R = I )
prdsvsca.k 
|- K = ( Base ` S )
prdsvsca.m 
|- .x. = ( .s ` P )
Assertion prdsvsca 
|- ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )

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 prdsbas.b 
 |-  B = ( Base ` P )
5 prdsbas.i 
 |-  ( ph -> dom R = I )
6 prdsvsca.k 
 |-  K = ( Base ` S )
7 prdsvsca.m 
 |-  .x. = ( .s ` P )
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 eqid 
 |-  ( .r ` P ) = ( .r ` P )
12 1 2 3 4 5 11 prdsmulr 
 |-  ( ph -> ( .r ` P ) = ( f e. B , g e. B |-> ( x e. I |-> ( ( f ` x ) ( .r ` ( R ` x ) ) ( g ` x ) ) ) ) )
13 eqidd 
 |-  ( ph -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
14 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 ) ) ) ) ) )
15 eqidd 
 |-  ( ph -> ( Xt_ ` ( TopOpen o. R ) ) = ( Xt_ ` ( TopOpen o. R ) ) )
16 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 ) ) } )
17 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* , < ) ) )
18 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 ) ) ) )
19 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 ) ) ) ) ) )
20 1 6 5 8 10 12 13 14 15 16 17 18 19 2 3 prdsval 
 |-  ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) ) ) ) ) >. } ) ) )
21 vscaid 
 |-  .s = Slot ( .s ` ndx )
22 ovssunirn 
 |-  ( f ( .s ` ( R ` x ) ) ( g ` x ) ) C_ U. ran ( .s ` ( R ` x ) )
23 21 strfvss 
 |-  ( .s ` ( R ` x ) ) C_ U. ran ( R ` x )
24 fvssunirn 
 |-  ( R ` x ) C_ U. ran R
25 rnss 
 |-  ( ( R ` x ) C_ U. ran R -> ran ( R ` x ) C_ ran U. ran R )
26 uniss 
 |-  ( ran ( R ` x ) C_ ran U. ran R -> U. ran ( R ` x ) C_ U. ran U. ran R )
27 24 25 26 mp2b 
 |-  U. ran ( R ` x ) C_ U. ran U. ran R
28 23 27 sstri 
 |-  ( .s ` ( R ` x ) ) C_ U. ran U. ran R
29 rnss 
 |-  ( ( .s ` ( R ` x ) ) C_ U. ran U. ran R -> ran ( .s ` ( R ` x ) ) C_ ran U. ran U. ran R )
30 uniss 
 |-  ( ran ( .s ` ( R ` x ) ) C_ ran U. ran U. ran R -> U. ran ( .s ` ( R ` x ) ) C_ U. ran U. ran U. ran R )
31 28 29 30 mp2b 
 |-  U. ran ( .s ` ( R ` x ) ) C_ U. ran U. ran U. ran R
32 22 31 sstri 
 |-  ( f ( .s ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R
33 ovex 
 |-  ( f ( .s ` ( R ` x ) ) ( g ` x ) ) e. _V
34 33 elpw 
 |-  ( ( f ( .s ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R <-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R )
35 32 34 mpbir 
 |-  ( f ( .s ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R
36 35 a1i 
 |-  ( ( ph /\ x e. I ) -> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) e. ~P U. ran U. ran U. ran R )
37 36 fmpttd 
 |-  ( ph -> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R )
38 rnexg 
 |-  ( R e. W -> ran R e. _V )
39 uniexg 
 |-  ( ran R e. _V -> U. ran R e. _V )
40 3 38 39 3syl 
 |-  ( ph -> U. ran R e. _V )
41 rnexg 
 |-  ( U. ran R e. _V -> ran U. ran R e. _V )
42 uniexg 
 |-  ( ran U. ran R e. _V -> U. ran U. ran R e. _V )
43 40 41 42 3syl 
 |-  ( ph -> U. ran U. ran R e. _V )
44 rnexg 
 |-  ( U. ran U. ran R e. _V -> ran U. ran U. ran R e. _V )
45 uniexg 
 |-  ( ran U. ran U. ran R e. _V -> U. ran U. ran U. ran R e. _V )
46 pwexg 
 |-  ( U. ran U. ran U. ran R e. _V -> ~P U. ran U. ran U. ran R e. _V )
47 43 44 45 46 4syl 
 |-  ( ph -> ~P U. ran U. ran U. ran R e. _V )
48 3 dmexd 
 |-  ( ph -> dom R e. _V )
49 5 48 eqeltrrd 
 |-  ( ph -> I e. _V )
50 47 49 elmapd 
 |-  ( ph -> ( ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) : I --> ~P U. ran U. ran U. ran R ) )
51 37 50 mpbird 
 |-  ( ph -> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
52 51 ralrimivw 
 |-  ( ph -> A. g e. B ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
53 52 ralrimivw 
 |-  ( ph -> A. f e. K A. g e. B ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) )
54 eqid 
 |-  ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) )
55 54 fmpo 
 |-  ( A. f e. K A. g e. B ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) e. ( ~P U. ran U. ran U. ran R ^m I ) <-> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) : ( K X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) )
56 53 55 sylib 
 |-  ( ph -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) : ( K X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) )
57 6 fvexi 
 |-  K e. _V
58 4 fvexi 
 |-  B e. _V
59 57 58 xpex 
 |-  ( K X. B ) e. _V
60 ovex 
 |-  ( ~P U. ran U. ran U. ran R ^m I ) e. _V
61 fex2 
 |-  ( ( ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) : ( K X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) /\ ( K X. B ) e. _V /\ ( ~P U. ran U. ran U. ran R ^m I ) e. _V ) -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
62 59 60 61 mp3an23 
 |-  ( ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) : ( K X. B ) --> ( ~P U. ran U. ran U. ran R ^m I ) -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
63 56 62 syl 
 |-  ( ph -> ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) e. _V )
64 snsstp2 
 |-  { <. ( .s ` ndx ) , ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ssun2 
 |-  { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) ) ) ) ) >. } )
66 64 65 sstri 
 |-  { <. ( .s ` ndx ) , ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) ) ) ) ) >. } )
67 ssun1 
 |-  ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) ) ) ) ) >. } ) )
68 66 67 sstri 
 |-  { <. ( .s ` ndx ) , ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( f e. K , 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 ) ) ) ) ) >. } ) )
69 20 7 21 63 68 prdsvallem 
 |-  ( ph -> .x. = ( f e. K , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )