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

Proof

Step	Hyp	Ref	Expression
1		rngcbas.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
2		rngcbas.b	$$⊢B={\mathrm{Base}}_C$$
3		rngcbas.u	$$⊢\phi \to U\in V$$
4	1 2 3	rngcbas	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
5		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
6	1 2 3 5	rngchomfval	$$⊢\phi \to \mathrm{Hom}\left(C\right)={\mathrm{RngHom}\upharpoonright }_{\left(B\times B\right)}$$
7	4 6	rnghmresfn	$$⊢\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)$$