Metamath Proof Explorer


Theorem rhmsubclem2

Description: Lemma 2 for rhmsubc . (Contributed by AV, 2-Mar-2020)

Ref Expression
Hypotheses rngcrescrhm.u φUV
rngcrescrhm.c C=RngCatU
rngcrescrhm.r φR=RingU
rngcrescrhm.h H=RingHomR×R
Assertion rhmsubclem2 φXRYRXHY=XRingHomY

Proof

Step Hyp Ref Expression
1 rngcrescrhm.u φUV
2 rngcrescrhm.c C=RngCatU
3 rngcrescrhm.r φR=RingU
4 rngcrescrhm.h H=RingHomR×R
5 opelxpi XRYRXYR×R
6 5 3adant1 φXRYRXYR×R
7 6 fvresd φXRYRRingHomR×RXY=RingHomXY
8 df-ov XHY=HXY
9 4 fveq1i HXY=RingHomR×RXY
10 8 9 eqtri XHY=RingHomR×RXY
11 df-ov XRingHomY=RingHomXY
12 7 10 11 3eqtr4g φXRYRXHY=XRingHomY