rhmsubclem2

	Ref	Expression
Hypotheses	rngcrescrhm.u	$⊢ φ \to U \in V$
	rngcrescrhm.c	$⊢ C = RngCat (U)$
	rngcrescrhm.r	$⊢ φ \to R = Ring \cap U$
	rngcrescrhm.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
Assertion	rhmsubclem2	$⊢ (φ \land X \in R \land Y \in R) \to X H Y = X RingHom Y$

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

Metamath Proof Explorer