Metamath Proof Explorer


Theorem dfrngc2

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

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

Proof

Step Hyp Ref Expression
1 dfrngc2.c
 |-  C = ( RngCat ` U )
2 dfrngc2.u
 |-  ( ph -> U e. V )
3 dfrngc2.b
 |-  ( ph -> B = ( U i^i Rng ) )
4 dfrngc2.h
 |-  ( ph -> H = ( RngHomo |` ( B X. B ) ) )
5 dfrngc2.o
 |-  ( ph -> .x. = ( comp ` ( ExtStrCat ` U ) ) )
6 1 2 3 4 rngcval
 |-  ( 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 Rng ) e. _V )
10 2 9 syl
 |-  ( ph -> ( U i^i Rng ) e. _V )
11 3 10 eqeltrd
 |-  ( ph -> B e. _V )
12 3 4 rnghmresfn
 |-  ( 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 rnghmfn
 |-  RngHomo Fn ( Rng X. Rng )
25 fnfun
 |-  ( RngHomo Fn ( Rng X. Rng ) -> Fun RngHomo )
26 24 25 mp1i
 |-  ( ph -> Fun RngHomo )
27 sqxpexg
 |-  ( B e. _V -> ( B X. B ) e. _V )
28 11 27 syl
 |-  ( ph -> ( B X. B ) e. _V )
29 resfunexg
 |-  ( ( Fun RngHomo /\ ( B X. B ) e. _V ) -> ( RngHomo |` ( B X. B ) ) e. _V )
30 26 28 29 syl2anc
 |-  ( ph -> ( RngHomo |` ( B X. B ) ) e. _V )
31 4 30 eqeltrd
 |-  ( ph -> H e. _V )
32 inss1
 |-  ( U i^i Rng ) 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. >. } )