Metamath Proof Explorer

Theorem prdshom

Description: Structure product hom-sets. (Contributed by Mario Carneiro, 7-Jan-2017) (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 )
prdshom.h 
|- H = ( Hom ` P )
Assertion prdshom 
|- ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( 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 prdshom.h 
 |-  H = ( Hom ` 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 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 eqid 
 |-  ( .s ` P ) = ( .s ` P )
14 1 2 3 4 5 7 13 prdsvsca 
 |-  ( ph -> ( .s ` P ) = ( f e. ( Base ` S ) , g e. B |-> ( x e. I |-> ( f ( .s ` ( R ` x ) ) ( g ` x ) ) ) ) )
15 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 ) ) ) ) ) )
16 eqid 
 |-  ( TopSet ` P ) = ( TopSet ` P )
17 1 2 3 4 5 16 prdstset 
 |-  ( ph -> ( TopSet ` P ) = ( Xt_ ` ( TopOpen o. R ) ) )
18 eqid 
 |-  ( le ` P ) = ( le ` P )
19 1 2 3 4 5 18 prdsle 
 |-  ( ph -> ( le ` P ) = { <. f , g >. | ( { f , g } C_ B /\ A. x e. I ( f ` x ) ( le ` ( R ` x ) ) ( g ` x ) ) } )
20 eqid 
 |-  ( dist ` P ) = ( dist ` P )
21 1 2 3 4 5 20 prdsds 
 |-  ( ph -> ( dist ` P ) = ( f e. B , g e. B |-> sup ( ( ran ( x e. I |-> ( ( f ` x ) ( dist ` ( R ` x ) ) ( g ` x ) ) ) u. { 0 } ) , RR* , < ) ) )
22 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 ) ) ) )
23 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 ) ) ) ) ) )
24 1 7 5 8 10 12 14 15 17 19 21 22 23 2 3 prdsval 
 |-  ( ph -> P = ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( .s ` P ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } ) ) )
25 homid 
 |-  Hom = Slot ( Hom ` ndx )
26 ovssunirn 
 |-  ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ U. ran ( Hom ` ( R ` x ) )
27 25 strfvss 
 |-  ( Hom ` ( R ` x ) ) C_ U. ran ( R ` x )
28 fvssunirn 
 |-  ( R ` x ) C_ U. ran R
29 rnss 
 |-  ( ( R ` x ) C_ U. ran R -> ran ( R ` x ) C_ ran U. ran R )
30 uniss 
 |-  ( ran ( R ` x ) C_ ran U. ran R -> U. ran ( R ` x ) C_ U. ran U. ran R )
31 28 29 30 mp2b 
 |-  U. ran ( R ` x ) C_ U. ran U. ran R
32 27 31 sstri 
 |-  ( Hom ` ( R ` x ) ) C_ U. ran U. ran R
33 rnss 
 |-  ( ( Hom ` ( R ` x ) ) C_ U. ran U. ran R -> ran ( Hom ` ( R ` x ) ) C_ ran U. ran U. ran R )
34 uniss 
 |-  ( ran ( Hom ` ( R ` x ) ) C_ ran U. ran U. ran R -> U. ran ( Hom ` ( R ` x ) ) C_ U. ran U. ran U. ran R )
35 32 33 34 mp2b 
 |-  U. ran ( Hom ` ( R ` x ) ) C_ U. ran U. ran U. ran R
36 26 35 sstri 
 |-  ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R
37 36 rgenw 
 |-  A. x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R
38 ss2ixp 
 |-  ( A. x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ U. ran U. ran U. ran R -> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ X_ x e. I U. ran U. ran U. ran R )
39 37 38 ax-mp 
 |-  X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ X_ x e. I U. ran U. ran U. ran R
40 3 dmexd 
 |-  ( ph -> dom R e. _V )
41 5 40 eqeltrrd 
 |-  ( ph -> I e. _V )
42 rnexg 
 |-  ( R e. W -> ran R e. _V )
43 uniexg 
 |-  ( ran R e. _V -> U. ran R e. _V )
44 3 42 43 3syl 
 |-  ( ph -> U. ran R e. _V )
45 rnexg 
 |-  ( U. ran R e. _V -> ran U. ran R e. _V )
46 uniexg 
 |-  ( ran U. ran R e. _V -> U. ran U. ran R e. _V )
47 44 45 46 3syl 
 |-  ( ph -> U. ran U. ran R e. _V )
48 rnexg 
 |-  ( U. ran U. ran R e. _V -> ran U. ran U. ran R e. _V )
49 uniexg 
 |-  ( ran U. ran U. ran R e. _V -> U. ran U. ran U. ran R e. _V )
50 47 48 49 3syl 
 |-  ( ph -> U. ran U. ran U. ran R e. _V )
51 ixpconstg 
 |-  ( ( I e. _V /\ U. ran U. ran U. ran R e. _V ) -> X_ x e. I U. ran U. ran U. ran R = ( U. ran U. ran U. ran R ^m I ) )
52 41 50 51 syl2anc 
 |-  ( ph -> X_ x e. I U. ran U. ran U. ran R = ( U. ran U. ran U. ran R ^m I ) )
53 39 52 sseqtrid 
 |-  ( ph -> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ ( U. ran U. ran U. ran R ^m I ) )
54 ovex 
 |-  ( U. ran U. ran U. ran R ^m I ) e. _V
55 54 elpw2 
 |-  ( X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran R ^m I ) <-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) C_ ( U. ran U. ran U. ran R ^m I ) )
56 53 55 sylibr 
 |-  ( ph -> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran R ^m I ) )
57 56 ralrimivw 
 |-  ( ph -> A. g e. B X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran R ^m I ) )
58 57 ralrimivw 
 |-  ( ph -> A. f e. B A. g e. B X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran R ^m I ) )
59 eqid 
 |-  ( 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 ) ) )
60 59 fmpo 
 |-  ( A. f e. B A. g e. B X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) e. ~P ( U. ran U. ran U. ran R ^m I ) <-> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) : ( B X. B ) --> ~P ( U. ran U. ran U. ran R ^m I ) )
61 58 60 sylib 
 |-  ( ph -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) : ( B X. B ) --> ~P ( U. ran U. ran U. ran R ^m I ) )
62 4 fvexi 
 |-  B e. _V
63 62 62 xpex 
 |-  ( B X. B ) e. _V
64 63 a1i 
 |-  ( ph -> ( B X. B ) e. _V )
65 54 pwex 
 |-  ~P ( U. ran U. ran U. ran R ^m I ) e. _V
66 65 a1i 
 |-  ( ph -> ~P ( U. ran U. ran U. ran R ^m I ) e. _V )
67 fex2 
 |-  ( ( ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( 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_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) e. _V )
68 61 64 66 67 syl3anc 
 |-  ( ph -> ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) e. _V )
69 snsspr1 
 |-  { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. } C_ { <. ( 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 ) ) ) ) ) >. }
70 ssun2 
 |-  { <. ( 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 ) ) ) ) ) >. } C_ ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } )
71 69 70 sstri 
 |-  { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. } C_ ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } )
72 ssun2 
 |-  ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } ) C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( .s ` P ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } ) )
73 71 72 sstri 
 |-  { <. ( Hom ` ndx ) , ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) >. } C_ ( ( { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , ( +g ` P ) >. , <. ( .r ` ndx ) , ( .r ` P ) >. } u. { <. ( Scalar ` ndx ) , S >. , <. ( .s ` ndx ) , ( .s ` P ) >. , <. ( .i ` ndx ) , ( f e. B , g e. B |-> ( S gsum ( x e. I |-> ( ( f ` x ) ( .i ` ( R ` x ) ) ( g ` x ) ) ) ) ) >. } ) u. ( { <. ( TopSet ` ndx ) , ( TopSet ` P ) >. , <. ( le ` ndx ) , ( le ` P ) >. , <. ( dist ` ndx ) , ( dist ` P ) >. } 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 ) ) ) ) ) >. } ) )
74 24 6 25 68 73 prdsbaslem 
 |-  ( ph -> H = ( f e. B , g e. B |-> X_ x e. I ( ( f ` x ) ( Hom ` ( R ` x ) ) ( g ` x ) ) ) )