This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rngchomfeqhom

Description: The functionalized Hom-set operation equals the Hom-set operation in the category of non-unital rings (in a universe). (Contributed by AV, 9-Mar-2020)

Ref Expression
Hypotheses rngcbas.c 
|- C = ( RngCat ` U )
rngcbas.b 
|- B = ( Base ` C )
rngcbas.u 
|- ( ph -> U e. V )
Assertion rngchomfeqhom 
|- ( ph -> ( Homf ` C ) = ( Hom ` C ) )

Proof

Step Hyp Ref Expression
1 rngcbas.c 
 |-  C = ( RngCat ` U )
2 rngcbas.b 
 |-  B = ( Base ` C )
3 rngcbas.u 
 |-  ( ph -> U e. V )
4 1 2 3 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
5 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
6 1 2 3 5 rngchomfval 
 |-  ( ph -> ( Hom ` C ) = ( RngHom |` ( B X. B ) ) )
7 4 6 rnghmresfn 
 |-  ( ph -> ( Hom ` C ) Fn ( B X. B ) )
8 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
9 8 2 5 fnhomeqhomf 
 |-  ( ( Hom ` C ) Fn ( B X. B ) -> ( Homf ` C ) = ( Hom ` C ) )
10 7 9 syl 
 |-  ( ph -> ( Homf ` C ) = ( Hom ` C ) )