Metamath Proof Explorer

Theorem ringchomfvalALTV

Description: Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringcbasALTV.c 
|- C = ( RingCatALTV ` U )
ringcbasALTV.b 
|- B = ( Base ` C )
ringcbasALTV.u 
|- ( ph -> U e. V )
ringchomfvalALTV.h 
|- H = ( Hom ` C )
Assertion ringchomfvalALTV 
|- ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c 
 |-  C = ( RingCatALTV ` U )
2 ringcbasALTV.b 
 |-  B = ( Base ` C )
3 ringcbasALTV.u 
 |-  ( ph -> U e. V )
4 ringchomfvalALTV.h 
 |-  H = ( Hom ` C )
5 1 2 3 ringcbasALTV 
 |-  ( ph -> B = ( U i^i Ring ) )
6 eqidd 
 |-  ( ph -> ( x e. B , y e. B |-> ( x RingHom y ) ) = ( x e. B , y e. B |-> ( x RingHom y ) ) )
7 eqidd 
 |-  ( ph -> ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) = ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) )
8 1 3 5 6 7 ringcvalALTV 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } )
9 8 fveq2d 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) )
10 4 9 syl5eq 
 |-  ( ph -> H = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) )
11 2 fvexi 
 |-  B e. _V
12 11 11 mpoex 
 |-  ( x e. B , y e. B |-> ( x RingHom y ) ) e. _V
13 catstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } Struct <. 1 , ; 1 5 >.
14 homid 
 |-  Hom = Slot ( Hom ` ndx )
15 snsstp2 
 |-  { <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. }
16 13 14 15 strfv 
 |-  ( ( x e. B , y e. B |-> ( x RingHom y ) ) e. _V -> ( x e. B , y e. B |-> ( x RingHom y ) ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) )
17 12 16 mp1i 
 |-  ( ph -> ( x e. B , y e. B |-> ( x RingHom y ) ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RingHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RingHom z ) , g e. ( ( 1st ` v ) RingHom ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) )
18 10 17 eqtr4d 
 |-  ( ph -> H = ( x e. B , y e. B |-> ( x RingHom y ) ) )