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

Metamath Proof Explorer

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

Proof

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