Metamath Proof Explorer

Theorem rhmresel

Description: An element of the unital ring homomorphisms restricted to a subset of unital rings is a unital ring homomorphism. (Contributed by AV, 10-Mar-2020)

		Ref	Expression
	Hypothesis	rhmresel.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
	Assertion	rhmresel	$⊢ (φ \land (X \in B \land Y \in B) \land F \in (X H Y)) \to F \in (X RingHom Y)$

Proof

Step	Hyp	Ref	Expression
1		rhmresel.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
2	1	adantr	$⊢ (φ \land (X \in B \land Y \in B)) \to H = {RingHom ↾}_{(B \times B)}$
3	2	oveqd	$⊢ (φ \land (X \in B \land Y \in B)) \to X H Y = X ({RingHom ↾}_{(B \times B)}) Y$
4		ovres	$⊢ (X \in B \land Y \in B) \to X ({RingHom ↾}_{(B \times B)}) Y = X RingHom Y$
5	4	adantl	$⊢ (φ \land (X \in B \land Y \in B)) \to X ({RingHom ↾}_{(B \times B)}) Y = X RingHom Y$
6	3 5	eqtrd	$⊢ (φ \land (X \in B \land Y \in B)) \to X H Y = X RingHom Y$
7	6	eleq2d	$⊢ (φ \land (X \in B \land Y \in B)) \to (F \in (X H Y) \leftrightarrow F \in (X RingHom Y))$
8	7	biimp3a	$⊢ (φ \land (X \in B \land Y \in B) \land F \in (X H Y)) \to F \in (X RingHom Y)$