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=\mathrm{RingCat}\left(U\right)$$
	ringcbas.b	$$⊢B={\mathrm{Base}}_C$$
	ringcbas.u	$$⊢\phi \to U\in V$$
Assertion	ringchomfeqhom	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{Hom}\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringcbas.c	$$⊢C=\mathrm{RingCat}\left(U\right)$$
2		ringcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		ringcbas.u	$$⊢\phi \to U\in V$$
4	1 2 3	ringcbas	$$⊢\phi \to B=U\cap \mathrm{Ring}$$
5		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
6	1 2 3 5	ringchomfval	$$⊢\phi \to \mathrm{Hom}\left(C\right)={\mathrm{RingHom}\upharpoonright }_{\left(B\times B\right)}$$
7	4 6	rhmresfn	$$⊢\phi \to \mathrm{Hom}\left(C\right)Fn\left(B\times B\right)$$
8		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
9	8 2 5	fnhomeqhomf	$$⊢\mathrm{Hom}\left(C\right)Fn\left(B\times B\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{Hom}\left(C\right)$$
10	7 9	syl	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{Hom}\left(C\right)$$