Theorem rhmsubclem2

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

	Ref	Expression
Hypotheses	rngcrescrhm.u	$$⊢\phi \to U\in V$$
	rngcrescrhm.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	rngcrescrhm.r	$$⊢\phi \to R=\mathrm{Ring}\cap U$$
	rngcrescrhm.h	$$⊢H={\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}$$
Assertion	rhmsubclem2	$$⊢\left(\phi \wedge X\in R\wedge Y\in R\right)\to XHY=X\mathrm{RingHom}Y$$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	$$⊢\phi \to U\in V$$
2		rngcrescrhm.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
3		rngcrescrhm.r	$$⊢\phi \to R=\mathrm{Ring}\cap U$$
4		rngcrescrhm.h	$$⊢H={\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}$$
5		opelxpi	$$⊢\left(X\in R\wedge Y\in R\right)\to ⟨X,Y⟩\in \left(R\times R\right)$$
6	5	3adant1	$$⊢\left(\phi \wedge X\in R\wedge Y\in R\right)\to ⟨X,Y⟩\in \left(R\times R\right)$$
7	6	fvresd	$$⊢\left(\phi \wedge X\in R\wedge Y\in R\right)\to \left({\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}\right)\left(⟨X,Y⟩\right)=\mathrm{RingHom}\left(⟨X,Y⟩\right)$$
8		df-ov	$$⊢XHY=H\left(⟨X,Y⟩\right)$$
9	4	fveq1i	$$⊢H\left(⟨X,Y⟩\right)=\left({\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}\right)\left(⟨X,Y⟩\right)$$
10	8 9	eqtri	$$⊢XHY=\left({\mathrm{RingHom}\upharpoonright }_{\left(R\times R\right)}\right)\left(⟨X,Y⟩\right)$$
11		df-ov	$$⊢X\mathrm{RingHom}Y=\mathrm{RingHom}\left(⟨X,Y⟩\right)$$
12	7 10 11	3eqtr4g	$$⊢\left(\phi \wedge X\in R\wedge Y\in R\right)\to XHY=X\mathrm{RingHom}Y$$