Metamath Proof Explorer


Theorem ringchomALTV

Description: Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses ringcbasALTV.c C=RingCatALTVU
ringcbasALTV.b B=BaseC
ringcbasALTV.u φUV
ringchomfvalALTV.h H=HomC
ringchomALTV.x φXB
ringchomALTV.y φYB
Assertion ringchomALTV φXHY=XRingHomY

Proof

Step Hyp Ref Expression
1 ringcbasALTV.c C=RingCatALTVU
2 ringcbasALTV.b B=BaseC
3 ringcbasALTV.u φUV
4 ringchomfvalALTV.h H=HomC
5 ringchomALTV.x φXB
6 ringchomALTV.y φYB
7 1 2 3 4 ringchomfvalALTV φH=xB,yBxRingHomy
8 oveq12 x=Xy=YxRingHomy=XRingHomY
9 8 adantl φx=Xy=YxRingHomy=XRingHomY
10 ovexd φXRingHomYV
11 7 9 5 6 10 ovmpod φXHY=XRingHomY