Metamath Proof Explorer


Theorem rngchom

Description: Set of arrows of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngcbas.c C=RngCatU
rngcbas.b B=BaseC
rngcbas.u φUV
rngchomfval.h H=HomC
rngchom.x φXB
rngchom.y φYB
Assertion rngchom φXHY=XRngHomoY

Proof

Step Hyp Ref Expression
1 rngcbas.c C=RngCatU
2 rngcbas.b B=BaseC
3 rngcbas.u φUV
4 rngchomfval.h H=HomC
5 rngchom.x φXB
6 rngchom.y φYB
7 1 2 3 4 rngchomfval φH=RngHomoB×B
8 7 oveqd φXHY=XRngHomoB×BY
9 5 6 ovresd φXRngHomoB×BY=XRngHomoY
10 8 9 eqtrd φXHY=XRngHomoY