Theorem ringchomfeqhom

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

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

Proof

Step	Hyp	Ref	Expression
1		ringcbas.c	|- C = ( RingCat ` U )
2		ringcbas.b	|- B = ( Base ` C )
3		ringcbas.u	|- ( ph -> U e. V )
4	1 2 3	ringcbas	|- ( ph -> B = ( U i^i Ring ) )
5		eqid	|- ( Hom ` C ) = ( Hom ` C )
6	1 2 3 5	ringchomfval	|- ( ph -> ( Hom ` C ) = ( RingHom |` ( B X. B ) ) )
7	4 6	rhmresfn	|- ( 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 ) )