Metamath Proof Explorer

Theorem rngccofvalALTV

Description: Composition in the category of non-unital rings. (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbasALTV.c 
|- C = ( RngCatALTV ` U )
rngcbasALTV.b 
|- B = ( Base ` C )
rngcbasALTV.u 
|- ( ph -> U e. V )
rngccofvalALTV.o 
|- .x. = ( comp ` C )
Assertion rngccofvalALTV 
|- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )

Proof

Step Hyp Ref Expression
1 rngcbasALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngcbasALTV.b 
 |-  B = ( Base ` C )
3 rngcbasALTV.u 
 |-  ( ph -> U e. V )
4 rngccofvalALTV.o 
 |-  .x. = ( comp ` C )
5 1 2 3 rngcbasALTV 
 |-  ( ph -> B = ( U i^i Rng ) )
6 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
7 1 2 3 6 rngchomfvalALTV 
 |-  ( ph -> ( Hom ` C ) = ( x e. B , y e. B |-> ( x RngHomo y ) ) )
8 eqidd 
 |-  ( ph -> ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
9 1 3 5 7 8 rngcvalALTV 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
10 9 fveq2d 
 |-  ( ph -> ( comp ` C ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } ) )
11 2 fvexi 
 |-  B e. _V
12 sqxpexg 
 |-  ( B e. _V -> ( B X. B ) e. _V )
13 11 12 ax-mp 
 |-  ( B X. B ) e. _V
14 13 11 mpoex 
 |-  ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) e. _V
15 catstr 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } Struct <. 1 , ; 1 5 >.
16 ccoid 
 |-  comp = Slot ( comp ` ndx )
17 snsstp3 
 |-  { <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. }
18 15 16 17 strfv 
 |-  ( ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) e. _V -> ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } ) )
19 14 18 ax-mp 
 |-  ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) = ( comp ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( Hom ` C ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
20 10 4 19 3eqtr4g 
 |-  ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHomo z ) , f e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( g o. f ) ) ) )