# Metamath Proof Explorer

## Theorem ringchom

Description: Set of arrows of the category of unital rings (in a universe). (Contributed by AV, 14-Feb-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}$
ringchomfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
ringchom.x ${⊢}{\phi }\to {X}\in {B}$
ringchom.y ${⊢}{\phi }\to {Y}\in {B}$
Assertion ringchom ${⊢}{\phi }\to {X}{H}{Y}={X}\mathrm{RingHom}{Y}$

### 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 ringchomfval.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
5 ringchom.x ${⊢}{\phi }\to {X}\in {B}$
6 ringchom.y ${⊢}{\phi }\to {Y}\in {B}$
7 1 2 3 4 ringchomfval ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
8 7 oveqd ${⊢}{\phi }\to {X}{H}{Y}={X}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right){Y}$
9 5 6 ovresd ${⊢}{\phi }\to {X}\left({\mathrm{RingHom}↾}_{\left({B}×{B}\right)}\right){Y}={X}\mathrm{RingHom}{Y}$
10 8 9 eqtrd ${⊢}{\phi }\to {X}{H}{Y}={X}\mathrm{RingHom}{Y}$