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	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
	rngcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	rngcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
Assertion	rngchomfeqhom	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		rngcbas.c	⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2		rngcbas.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		rngcbas.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4	1 2 3	rngcbas	⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
5		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6	1 2 3 5	rngchomfval	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) = ( RngHomo ↾ ( 𝐵 × 𝐵 ) ) )
7	4 6	rnghmresfn	⊢ ( 𝜑 → ( Hom ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) )
8		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
9	8 2 5	fnhomeqhomf	⊢ ( ( Hom ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) → ( Homf ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
10	7 9	syl	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )