Step |
Hyp |
Ref |
Expression |
1 |
|
rngcbasALTV.c |
|- C = ( RngCatALTV ` U ) |
2 |
|
rngcbasALTV.b |
|- B = ( Base ` C ) |
3 |
|
rngcbasALTV.u |
|- ( ph -> U e. V ) |
4 |
|
rngchomfvalALTV.h |
|- H = ( Hom ` C ) |
5 |
1 2 3
|
rngcbasALTV |
|- ( ph -> B = ( U i^i Rng ) ) |
6 |
|
eqidd |
|- ( ph -> ( x e. B , y e. B |-> ( x RngHomo y ) ) = ( x e. B , y e. B |-> ( x RngHomo y ) ) ) |
7 |
|
eqidd |
|- ( ph -> ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) = ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) ) |
8 |
1 3 5 6 7
|
rngcvalALTV |
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) |
9 |
8
|
fveq2d |
|- ( ph -> ( Hom ` C ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) ) |
10 |
4 9
|
syl5eq |
|- ( ph -> H = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) ) |
11 |
2
|
fvexi |
|- B e. _V |
12 |
11 11
|
mpoex |
|- ( x e. B , y e. B |-> ( x RngHomo y ) ) e. _V |
13 |
|
catstr |
|- { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 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 RngHomo y ) ) >. } C_ { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } |
16 |
13 14 15
|
strfv |
|- ( ( x e. B , y e. B |-> ( x RngHomo y ) ) e. _V -> ( x e. B , y e. B |-> ( x RngHomo y ) ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) ) |
17 |
12 16
|
mp1i |
|- ( ph -> ( x e. B , y e. B |-> ( x RngHomo y ) ) = ( Hom ` { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , ( x e. B , y e. B |-> ( x RngHomo y ) ) >. , <. ( comp ` ndx ) , ( v e. ( B X. B ) , z e. B |-> ( f e. ( ( 2nd ` v ) RngHomo z ) , g e. ( ( 1st ` v ) RngHomo ( 2nd ` v ) ) |-> ( f o. g ) ) ) >. } ) ) |
18 |
10 17
|
eqtr4d |
|- ( ph -> H = ( x e. B , y e. B |-> ( x RngHomo y ) ) ) |