Theorem rhmsubcALTVlem2

Description: Lemma 2 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$$⊢\phi \to U\in V$$
2		rngcrescrhmALTV.c	$$⊢C=\mathrm{RngCatALTV}\left(U\right)$$
3		rngcrescrhmALTV.r	$$⊢\phi \to R=\mathrm{Ring}\cap U$$
4		rngcrescrhmALTV.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$$