Metamath Proof Explorer

Theorem dfringc2

Description: Alternate definition of the category of unital rings (in a universe). (Contributed by AV, 16-Mar-2020)

Ref Expression
Hypotheses dfringc2.c 
|- C = ( RingCat ` U )
dfringc2.u 
|- ( ph -> U e. V )
dfringc2.b 
|- ( ph -> B = ( U i^i Ring ) )
dfringc2.h 
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
dfringc2.o 
|- ( ph -> .x. = ( comp ` ( ExtStrCat ` U ) ) )
Assertion dfringc2 
|- ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )

Proof

Step Hyp Ref Expression
1 dfringc2.c 
 |-  C = ( RingCat ` U )
2 dfringc2.u 
 |-  ( ph -> U e. V )
3 dfringc2.b 
 |-  ( ph -> B = ( U i^i Ring ) )
4 dfringc2.h 
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 dfringc2.o 
 |-  ( ph -> .x. = ( comp ` ( ExtStrCat ` U ) ) )
6 1 2 3 4 ringcval 
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )
7 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat H ) = ( ( ExtStrCat ` U ) |`cat H )
8 fvexd 
 |-  ( ph -> ( ExtStrCat ` U ) e. _V )
9 inex1g 
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
10 2 9 syl 
 |-  ( ph -> ( U i^i Ring ) e. _V )
11 3 10 eqeltrd 
 |-  ( ph -> B e. _V )
12 3 4 rhmresfn 
 |-  ( ph -> H Fn ( B X. B ) )
13 7 8 11 12 rescval2 
 |-  ( ph -> ( ( ExtStrCat ` U ) |`cat H ) = ( ( ( ExtStrCat ` U ) |`s B ) sSet <. ( Hom ` ndx ) , H >. ) )
14 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
15 eqidd 
 |-  ( ph -> ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) = ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) )
16 eqid 
 |-  ( comp ` ( ExtStrCat ` U ) ) = ( comp ` ( ExtStrCat ` U ) )
17 14 2 16 estrccofval 
 |-  ( ph -> ( comp ` ( ExtStrCat ` U ) ) = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )
18 5 17 eqtrd 
 |-  ( ph -> .x. = ( v e. ( U X. U ) , z e. U |-> ( g e. ( ( Base ` z ) ^m ( Base ` ( 2nd ` v ) ) ) , f e. ( ( Base ` ( 2nd ` v ) ) ^m ( Base ` ( 1st ` v ) ) ) |-> ( g o. f ) ) ) )
19 14 2 15 18 estrcval 
 |-  ( ph -> ( ExtStrCat ` U ) = { <. ( Base ` ndx ) , U >. , <. ( Hom ` ndx ) , ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) >. , <. ( comp ` ndx ) , .x. >. } )
20 mpoexga 
 |-  ( ( U e. V /\ U e. V ) -> ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V )
21 2 2 20 syl2anc 
 |-  ( ph -> ( x e. U , y e. U |-> ( ( Base ` y ) ^m ( Base ` x ) ) ) e. _V )
22 fvexd 
 |-  ( ph -> ( comp ` ( ExtStrCat ` U ) ) e. _V )
23 5 22 eqeltrd 
 |-  ( ph -> .x. e. _V )
24 rhmfn 
 |-  RingHom Fn ( Ring X. Ring )
25 fnfun 
 |-  ( RingHom Fn ( Ring X. Ring ) -> Fun RingHom )
26 24 25 mp1i 
 |-  ( ph -> Fun RingHom )
27 sqxpexg 
 |-  ( B e. _V -> ( B X. B ) e. _V )
28 11 27 syl 
 |-  ( ph -> ( B X. B ) e. _V )
29 resfunexg 
 |-  ( ( Fun RingHom /\ ( B X. B ) e. _V ) -> ( RingHom |` ( B X. B ) ) e. _V )
30 26 28 29 syl2anc 
 |-  ( ph -> ( RingHom |` ( B X. B ) ) e. _V )
31 4 30 eqeltrd 
 |-  ( ph -> H e. _V )
32 inss1 
 |-  ( U i^i Ring ) C_ U
33 3 32 eqsstrdi 
 |-  ( ph -> B C_ U )
34 19 2 21 23 31 33 estrres 
 |-  ( ph -> ( ( ( ExtStrCat ` U ) |`s B ) sSet <. ( Hom ` ndx ) , H >. ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )
35 6 13 34 3eqtrd 
 |-  ( ph -> C = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , .x. >. } )