Metamath Proof Explorer

Theorem rngcvalALTV

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

Ref Expression
Hypotheses rngcvalALTV.c 
|- C = ( RngCatALTV ` U )
rngcvalALTV.u 
|- ( ph -> U e. V )
rngcvalALTV.b 
|- ( ph -> B = ( U i^i Rng ) )
rngcvalALTV.h 
|- ( ph -> H = ( x e. B , y e. B |-> ( x RngHom y ) ) )
rngcvalALTV.o 
|- ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
Assertion rngcvalALTV 
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )

Proof

Step Hyp Ref Expression
1 rngcvalALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngcvalALTV.u 
 |-  ( ph -> U e. V )
3 rngcvalALTV.b 
 |-  ( ph -> B = ( U i^i Rng ) )
4 rngcvalALTV.h 
 |-  ( ph -> H = ( x e. B , y e. B |-> ( x RngHom y ) ) )
5 rngcvalALTV.o 
 |-  ( ph -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
6 df-rngcALTV 
 |-  RngCatALTV = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } )
7 6 a1i 
 |-  ( ph -> RngCatALTV = ( u e. _V |-> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } ) )
8 vex 
 |-  u e. _V
9 8 inex1 
 |-  ( u i^i Rng ) e. _V
10 9 a1i 
 |-  ( ( ph /\ u = U ) -> ( u i^i Rng ) e. _V )
11 ineq1 
 |-  ( u = U -> ( u i^i Rng ) = ( U i^i Rng ) )
12 11 adantl 
 |-  ( ( ph /\ u = U ) -> ( u i^i Rng ) = ( U i^i Rng ) )
13 3 adantr 
 |-  ( ( ph /\ u = U ) -> B = ( U i^i Rng ) )
14 12 13 eqtr4d 
 |-  ( ( ph /\ u = U ) -> ( u i^i Rng ) = B )
15 simpr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> b = B )
16 15 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( Base ` ndx ) , b >. = <. ( Base ` ndx ) , B >. )
17 eqidd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x RngHom y ) = ( x RngHom y ) )
18 15 15 17 mpoeq123dv 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x e. b , y e. b |-> ( x RngHom y ) ) = ( x e. B , y e. B |-> ( x RngHom y ) ) )
19 4 ad2antrr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> H = ( x e. B , y e. B |-> ( x RngHom y ) ) )
20 18 19 eqtr4d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( x e. b , y e. b |-> ( x RngHom y ) ) = H )
21 20 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHom y ) ) >. = <. ( Hom ` ndx ) , H >. )
22 15 sqxpeqd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( b X. b ) = ( B X. B ) )
23 eqidd 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) = ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) )
24 22 15 23 mpoeq123dv 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
25 5 ad2antrr 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> .x. = ( v e. ( B X. B ) , z e. B |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) )
26 24 25 eqtr4d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) = .x. )
27 26 opeq2d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. = <. ( comp ` ndx ) , .x. >. )
28 16 21 27 tpeq123d 
 |-  ( ( ( ph /\ u = U ) /\ b = B ) -> { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
29 10 14 28 csbied2 
 |-  ( ( ph /\ u = U ) -> [_ ( u i^i Rng ) / b ]_ { <. ( Base ` ndx ) , b >. , <. ( Hom ` ndx ) , ( x e. b , y e. b |-> ( x RngHom y ) ) >. , <. ( comp ` ndx ) , ( v e. ( b X. b ) , z e. b |-> ( g e. ( ( 2nd ` v ) RngHom z ) , f e. ( ( 1st ` v ) RngHom ( 2nd ` v ) ) |-> ( g o. f ) ) ) >. } = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
30 elex 
 |-  ( U e. V -> U e. _V )
31 2 30 syl 
 |-  ( ph -> U e. _V )
32 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V
33 32 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } e. _V )
34 7 29 31 33 fvmptd 
 |-  ( ph -> ( RngCatALTV ` U ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
35 1 34 eqtrid 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )