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 ) = ( RngHomo |` ( 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 ) )