Metamath Proof Explorer

Theorem rngcresringcat

Description: The restriction of the category of non-unital rings to the set of unital ring homomorphisms is the category of unital rings. (Contributed by AV, 16-Mar-2020)

Ref Expression
Hypotheses rhmsubcrngc.c 
|- C = ( RngCat ` U )
rhmsubcrngc.u 
|- ( ph -> U e. V )
rhmsubcrngc.b 
|- ( ph -> B = ( Ring i^i U ) )
rhmsubcrngc.h 
|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Assertion rngcresringcat 
|- ( ph -> ( C |`cat H ) = ( RingCat ` U ) )

Proof

Step Hyp Ref Expression
1 rhmsubcrngc.c 
 |-  C = ( RngCat ` U )
2 rhmsubcrngc.u 
 |-  ( ph -> U e. V )
3 rhmsubcrngc.b 
 |-  ( ph -> B = ( Ring i^i U ) )
4 rhmsubcrngc.h 
 |-  ( ph -> H = ( RingHom |` ( B X. B ) ) )
5 eqidd 
 |-  ( ph -> ( U i^i Rng ) = ( U i^i Rng ) )
6 eqidd 
 |-  ( ph -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) = ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) )
7 eqidd 
 |-  ( ph -> ( comp ` ( ExtStrCat ` U ) ) = ( comp ` ( ExtStrCat ` U ) ) )
8 1 2 5 6 7 dfrngc2 
 |-  ( ph -> C = { <. ( Base ` ndx ) , ( U i^i Rng ) >. , <. ( Hom ` ndx ) , ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) >. , <. ( comp ` ndx ) , ( comp ` ( ExtStrCat ` U ) ) >. } )
9 inex1g 
 |-  ( U e. V -> ( U i^i Rng ) e. _V )
10 2 9 syl 
 |-  ( ph -> ( U i^i Rng ) e. _V )
11 rnghmfn 
 |-  RngHomo Fn ( Rng X. Rng )
12 fnfun 
 |-  ( RngHomo Fn ( Rng X. Rng ) -> Fun RngHomo )
13 11 12 mp1i 
 |-  ( ph -> Fun RngHomo )
14 sqxpexg 
 |-  ( ( U i^i Rng ) e. _V -> ( ( U i^i Rng ) X. ( U i^i Rng ) ) e. _V )
15 10 14 syl 
 |-  ( ph -> ( ( U i^i Rng ) X. ( U i^i Rng ) ) e. _V )
16 resfunexg 
 |-  ( ( Fun RngHomo /\ ( ( U i^i Rng ) X. ( U i^i Rng ) ) e. _V ) -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) e. _V )
17 13 15 16 syl2anc 
 |-  ( ph -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) e. _V )
18 fvexd 
 |-  ( ph -> ( comp ` ( ExtStrCat ` U ) ) e. _V )
19 rhmfn 
 |-  RingHom Fn ( Ring X. Ring )
20 fnfun 
 |-  ( RingHom Fn ( Ring X. Ring ) -> Fun RingHom )
21 19 20 mp1i 
 |-  ( ph -> Fun RingHom )
22 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
23 3 22 eqtrdi 
 |-  ( ph -> B = ( U i^i Ring ) )
24 inex1g 
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
25 2 24 syl 
 |-  ( ph -> ( U i^i Ring ) e. _V )
26 23 25 eqeltrd 
 |-  ( ph -> B e. _V )
27 sqxpexg 
 |-  ( B e. _V -> ( B X. B ) e. _V )
28 26 27 syl 
 |-  ( ph -> ( B X. B ) e. _V )
29 resfunexg 
 |-  ( ( Fun RingHom /\ ( B X. B ) e. _V ) -> ( RingHom |` ( B X. B ) ) e. _V )
30 21 28 29 syl2anc 
 |-  ( ph -> ( RingHom |` ( B X. B ) ) e. _V )
31 4 30 eqeltrd 
 |-  ( ph -> H e. _V )
32 ringrng 
 |-  ( r e. Ring -> r e. Rng )
33 32 a1i 
 |-  ( ph -> ( r e. Ring -> r e. Rng ) )
34 33 ssrdv 
 |-  ( ph -> Ring C_ Rng )
35 34 ssrind 
 |-  ( ph -> ( Ring i^i U ) C_ ( Rng i^i U ) )
36 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
37 36 a1i 
 |-  ( ph -> ( U i^i Rng ) = ( Rng i^i U ) )
38 35 3 37 3sstr4d 
 |-  ( ph -> B C_ ( U i^i Rng ) )
39 8 10 17 18 31 38 estrres 
 |-  ( ph -> ( ( C |`s B ) sSet <. ( Hom ` ndx ) , H >. ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , ( comp ` ( ExtStrCat ` U ) ) >. } )
40 eqid 
 |-  ( C |`cat H ) = ( C |`cat H )
41 fvexd 
 |-  ( ph -> ( RngCat ` U ) e. _V )
42 1 41 eqeltrid 
 |-  ( ph -> C e. _V )
43 23 4 rhmresfn 
 |-  ( ph -> H Fn ( B X. B ) )
44 40 42 26 43 rescval2 
 |-  ( ph -> ( C |`cat H ) = ( ( C |`s B ) sSet <. ( Hom ` ndx ) , H >. ) )
45 eqid 
 |-  ( RingCat ` U ) = ( RingCat ` U )
46 45 2 23 4 7 dfringc2 
 |-  ( ph -> ( RingCat ` U ) = { <. ( Base ` ndx ) , B >. , <. ( Hom ` ndx ) , H >. , <. ( comp ` ndx ) , ( comp ` ( ExtStrCat ` U ) ) >. } )
47 39 44 46 3eqtr4d 
 |-  ( ph -> ( C |`cat H ) = ( RingCat ` U ) )