This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to U \in V$
	Assertion	ringchomfeqhom	$⊢ φ \to {Hom}_{𝑓} (C) = Hom (C)$

Proof

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