Metamath Proof Explorer

Theorem rnghmresel

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

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

Proof

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