Metamath Proof Explorer

Theorem rngcrescrhm

Description: The category of non-unital rings (in a universe) restricted to the ring homomorphisms between unital rings (in the same universe). (Contributed by AV, 1-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u 
|- ( ph -> U e. V )
rngcrescrhm.c 
|- C = ( RngCat ` U )
rngcrescrhm.r 
|- ( ph -> R = ( Ring i^i U ) )
rngcrescrhm.h 
|- H = ( RingHom |` ( R X. R ) )
Assertion rngcrescrhm 
|- ( ph -> ( C |`cat H ) = ( ( C |`s R ) sSet <. ( Hom ` ndx ) , H >. ) )

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u 
 |-  ( ph -> U e. V )
2 rngcrescrhm.c 
 |-  C = ( RngCat ` U )
3 rngcrescrhm.r 
 |-  ( ph -> R = ( Ring i^i U ) )
4 rngcrescrhm.h 
 |-  H = ( RingHom |` ( R X. R ) )
5 eqid 
 |-  ( C |`cat H ) = ( C |`cat H )
6 2 fvexi 
 |-  C e. _V
7 6 a1i 
 |-  ( ph -> C e. _V )
8 incom 
 |-  ( Ring i^i U ) = ( U i^i Ring )
9 3 8 eqtrdi 
 |-  ( ph -> R = ( U i^i Ring ) )
10 inex1g 
 |-  ( U e. V -> ( U i^i Ring ) e. _V )
11 1 10 syl 
 |-  ( ph -> ( U i^i Ring ) e. _V )
12 9 11 eqeltrd 
 |-  ( ph -> R e. _V )
13 inss1 
 |-  ( Ring i^i U ) C_ Ring
14 3 13 eqsstrdi 
 |-  ( ph -> R C_ Ring )
15 xpss12 
 |-  ( ( R C_ Ring /\ R C_ Ring ) -> ( R X. R ) C_ ( Ring X. Ring ) )
16 14 14 15 syl2anc 
 |-  ( ph -> ( R X. R ) C_ ( Ring X. Ring ) )
17 rhmfn 
 |-  RingHom Fn ( Ring X. Ring )
18 fnssresb 
 |-  ( RingHom Fn ( Ring X. Ring ) -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
19 17 18 mp1i 
 |-  ( ph -> ( ( RingHom |` ( R X. R ) ) Fn ( R X. R ) <-> ( R X. R ) C_ ( Ring X. Ring ) ) )
20 16 19 mpbird 
 |-  ( ph -> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
21 4 fneq1i 
 |-  ( H Fn ( R X. R ) <-> ( RingHom |` ( R X. R ) ) Fn ( R X. R ) )
22 20 21 sylibr 
 |-  ( ph -> H Fn ( R X. R ) )
23 5 7 12 22 rescval2 
 |-  ( ph -> ( C |`cat H ) = ( ( C |`s R ) sSet <. ( Hom ` ndx ) , H >. ) )